From 6573374f3ffde1ef21a2e3fff353cc1791d7be74 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 7 May 2024 22:22:30 +0200
Subject: [PATCH] No need to unseal here

---
 src/Init/Data/Nat/Div.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index 33645c4f9e6f..d570a32b24ee 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -95,7 +95,6 @@ protected def mod : @& Nat → @& Nat → Nat
 
 instance instMod : Mod Nat := ⟨Nat.mod⟩
 
-unseal Nat.modCore in
 protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
   match x, y with
   | 0, y =>