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

leanprover-community · May 8, 2024 · 450f571 · 450f571
1 parent e69cfc6
commit 450f571
Show file tree

Hide file tree

Showing 8 changed files with 0 additions and 18 deletions.
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Faces.lean b/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)]

diff --git a/Mathlib/CategoryTheory/ComposableArrows.lean b/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

diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
@@ -437,7 +437,6 @@ instance : Lattice (Fin (n + 1)) :=
 
 theorem last_pos' [NeZero n] : 0 < last n := NeZero.pos n
 
-unseal Nat.modCore in
 theorem one_lt_last [NeZero n] : 1 < last (n + 1) :=
   (lt_add_iff_pos_left 1).mpr (NeZero.pos n)
 
@@ -752,7 +751,6 @@ theorem succ_injective (n : ℕ) : Injective (@Fin.succ n) := (succEmb n).inject
 #align fin.succ_inj Fin.succ_inj
 #align fin.succ_ne_zero Fin.succ_ne_zero
 
-unseal Nat.modCore in
 @[simp]
 theorem succ_zero_eq_one' [NeZero n] : Fin.succ (0 : Fin n) = 1 := by
   cases n
@@ -1334,7 +1332,6 @@ theorem castPred_zero (h := last_pos.ne)  :
     castPred (0 : Fin (n + 2)) h = 0 := rfl
 #align fin.cast_pred_zero Fin.castPred_zero
 
-unseal Nat.modCore in
 @[simp]
 theorem castPred_one [NeZero n] (h := one_lt_last.ne) : castPred (1 : Fin (n + 2)) h = 1 := by
   cases n

diff --git a/Mathlib/Data/Fin/OrderHom.lean b/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))

diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/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

diff --git a/Mathlib/Data/Fin/VecNotation.lean b/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

diff --git a/Mathlib/GroupTheory/Perm/List.lean b/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')) :

diff --git a/Mathlib/GroupTheory/Perm/Sign.lean b/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⟩) =