No need to unseal here

leanprover · May 7, 2024 · 6573374 · 6573374
1 parent d7b152b
commit 6573374
Showing 1 changed file with 0 additions and 1 deletion.
diff --git 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 =>