less unseal Nat.modCore needed due to leanprover/lean4#4098

Mathlib/AlgebraicTopology/DoldKan/Faces.lean

@@ -140,7 +140,6 @@ theorem comp_Hσ_eq {Y : C} {n a q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFac
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.higher_faces_vanish.comp_Hσ_eq AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq
 
-unseal Nat.modCore in
 theorem comp_Hσ_eq_zero {Y : C} {n q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFacesVanish q φ)
     (hqn : n < q) : φ ≫ (Hσ q).f (n + 1) = 0 := by
   simp only [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl)]

Mathlib/CategoryTheory/ComposableArrows.lean

@@ -51,13 +51,6 @@ We'll soon provide finer grained options here, e.g. to turn off simprocs only in
 -/
 set_option simprocs false
 
-
-/-!
-This module contains many `Fin` literals like `1`, where we need to allow `1 % 2` to compute
-for a fair number of proofs by definitional equality in this module.
--/
-unseal Nat.modCore
-
 namespace CategoryTheory
 
 open Category

Mathlib/Data/Fin/OrderHom.lean

@@ -317,7 +317,6 @@ lemma rev_succAbove (p : Fin (n + 1)) (i : Fin n) :
     rev (succAbove p i) = succAbove (rev p) (rev i) := by
   rw [succAbove_rev_left, rev_rev]
 
-unseal Nat.modCore in
 --@[simp] -- Porting note: can be proved by `simp`
 theorem one_succAbove_zero {n : ℕ} : (1 : Fin (n + 2)).succAbove 0 = 0 := by
   rfl
@@ -339,7 +338,6 @@ theorem one_succAbove_succ {n : ℕ} (j : Fin n) :
   rwa [succ_zero_eq_one, zero_succAbove] at this
 #align fin.one_succ_above_succ Fin.one_succAbove_succ
 
-unseal Nat.modCore in
 @[simp]
 theorem one_succAbove_one {n : ℕ} : (1 : Fin (n + 3)).succAbove 1 = 2 := by
   have := succ_succAbove_succ (0 : Fin (n + 2)) (0 : Fin (n + 2))

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -79,7 +79,6 @@ theorem cons_succ : cons x p i.succ = p i := by simp [cons]
 theorem cons_zero : cons x p 0 = x := by simp [cons]
 #align fin.cons_zero Fin.cons_zero
 
-unseal Nat.modCore in
 @[simp]
 theorem cons_one {α : Fin (n + 2) → Type*} (x : α 0) (p : ∀ i : Fin n.succ, α i.succ) :
     cons x p 1 = p 0 := by

Mathlib/Data/Fin/VecNotation.lean

@@ -200,7 +200,6 @@ theorem vec_single_eq_const (a : α) : ![a] = fun _ => a :=
   funext <| Unique.forall_iff.2 rfl
 #align matrix.vec_single_eq_const Matrix.vec_single_eq_const
 
-unseal Nat.modCore in
 /-- `![a, b, ...] 1` is equal to `b`.
 
   The simplifier needs a special lemma for length `≥ 2`, in addition to

Mathlib/GroupTheory/Perm/List.lean

@@ -308,7 +308,6 @@ theorem formPerm_pow_apply_head (x : α) (l : List α) (h : Nodup (x :: l)) (n :
   simp
 #align list.form_perm_pow_apply_head List.formPerm_pow_apply_head
 
-unseal Nat.modCore in
 set_option linter.deprecated false in
 theorem formPerm_ext_iff {x y x' y' : α} {l l' : List α} (hd : Nodup (x :: y :: l))
     (hd' : Nodup (x' :: y' :: l')) :

Mathlib/GroupTheory/Perm/Sign.lean

@@ -246,7 +246,6 @@ theorem signAux_mul {n : ℕ} (f g : Perm (Fin n)) : signAux (f * g) = signAux f
       rfl
 #align equiv.perm.sign_aux_mul Equiv.Perm.signAux_mul
 
-unseal Nat.modCore in
 private theorem signAux_swap_zero_one' (n : ℕ) : signAux (swap (0 : Fin (n + 2)) 1) = -1 :=
   show _ = ∏ x : Σ_a : Fin (n + 2), Fin (n + 2) in {(⟨1, 0⟩ : Σa : Fin (n + 2), Fin (n + 2))},
       if (Equiv.swap 0 1) x.1 ≤ swap 0 1 x.2 then (-1 : ℤˣ) else 1 by
@@ -271,7 +270,6 @@ private theorem signAux_swap_zero_one' (n : ℕ) : signAux (swap (0 : Fin (n + 2
       · rw [swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt),
           swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'), if_neg ha₁.not_le]
 
-unseal Nat.modCore in
 set_option tactic.skipAssignedInstances false in
 private theorem signAux_swap_zero_one {n : ℕ} (hn : 2 ≤ n) :
     signAux (swap (⟨0, lt_of_lt_of_le (by decide) hn⟩ : Fin n) ⟨1, lt_of_lt_of_le (by decide) hn⟩) =

Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean

@@ -366,7 +366,7 @@ theorem div_four_left {a : ℤ} {b : ℕ} (ha4 : a % 4 = 0) (hb2 : b % 2 = 1) :
   rw [Int.mul_ediv_cancel_left _ (by decide), jacobiSym.mul_left,
     (by decide : (4 : ℤ) = (2 : ℕ) ^ 2), jacobiSym.sq_one' this, one_mul]
 
-unseal Nat.modCore in
+seal Nat.modCore in
 theorem even_odd {a : ℤ} {b : ℕ} (ha2 : a % 2 = 0) (hb2 : b % 2 = 1) :
     (if b % 8 = 3 ∨ b % 8 = 5 then -J(a / 2 | b) else J(a / 2 | b)) = J(a | b) := by
   obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha2