experiment: run hammers on Mathlib

.github/build.in.yml

@@ -559,11 +559,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
 
-      - name: build AesopTest (nightly-testing only)
-        # Only run on the mathlib4-nightly-testing repository
-        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
-        run: |
-          lake build AesopTest
+      # temporarily comment out
+      # - name: build AesopTest (nightly-testing only)
+      #   # Only run on the mathlib4-nightly-testing repository
+      #   if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+      #   run: |
+      #     lake build AesopTest
 
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.

.github/workflows/bors.yml

@@ -569,11 +569,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
 
-      - name: build AesopTest (nightly-testing only)
-        # Only run on the mathlib4-nightly-testing repository
-        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
-        run: |
-          lake build AesopTest
+      # temporarily comment out
+      # - name: build AesopTest (nightly-testing only)
+      #   # Only run on the mathlib4-nightly-testing repository
+      #   if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+      #   run: |
+      #     lake build AesopTest
 
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.

.github/workflows/build.yml

@@ -576,11 +576,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
 
-      - name: build AesopTest (nightly-testing only)
-        # Only run on the mathlib4-nightly-testing repository
-        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
-        run: |
-          lake build AesopTest
+      # temporarily comment out
+      # - name: build AesopTest (nightly-testing only)
+      #   # Only run on the mathlib4-nightly-testing repository
+      #   if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+      #   run: |
+      #     lake build AesopTest
 
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.

.github/workflows/build_fork.yml

@@ -573,11 +573,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
 
-      - name: build AesopTest (nightly-testing only)
-        # Only run on the mathlib4-nightly-testing repository
-        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
-        run: |
-          lake build AesopTest
+      # temporarily comment out
+      # - name: build AesopTest (nightly-testing only)
+      #   # Only run on the mathlib4-nightly-testing repository
+      #   if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+      #   run: |
+      #     lake build AesopTest
 
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.

Archive/Imo/Imo1988Q6.lean

@@ -233,14 +233,14 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
         rw [← sub_eq_zero, ← h_root]
         ring
       rw [hzx] at hpos
-      replace hpos : z * x + 1 > 0 := pos_of_mul_pos_left hpos (Int.ofNat_zero_le k)
+      replace hpos : z * x + 1 > 0 := pos_of_mul_pos_left hpos (Int.natCast_nonneg k)
       replace hpos : z * x ≥ 0 := Int.le_of_lt_add_one hpos
       apply nonneg_of_mul_nonneg_left hpos (mod_cast hx)
     · contrapose! hV₀ with x_lt_z
       apply ne_of_gt
       calc
         z * y > x * x := by apply mul_lt_mul' <;> omega
-        _ ≥ x * x - k := sub_le_self _ (Int.ofNat_zero_le k)
+        _ ≥ x * x - k := sub_le_self _ (Int.natCast_nonneg k)
   · -- There is no base case in this application of Vieta jumping.
     simp
 

Archive/Imo/Imo1997Q3.lean

@@ -82,7 +82,7 @@ lemma sign_eq_of_contra
       rw [mem_compl, mem_insert, mem_singleton, not_or] at mj
       exact swap_apply_of_ne_of_ne mj.1 mj.2
     rw [cg, add_sub_add_right_eq_sub,
-      sum_pair (castSucc_lt_succ _).ne, sum_pair (castSucc_lt_succ _).ne,
+      sum_pair castSucc_lt_succ.ne, sum_pair castSucc_lt_succ.ne,
       Perm.mul_apply, Perm.mul_apply, ← hi, swap_apply_left, swap_apply_right,
       add_comm, add_sub_add_comm, ← sub_mul, ← sub_mul,
       val_succ, coe_castSucc, Nat.cast_add, Nat.cast_one, add_sub_cancel_left, sub_add_cancel_left,

Archive/Imo/Imo2024Q5.lean

@@ -387,7 +387,7 @@ lemma Path.findFstEq_fst_sub_one_mem (p : Path N) {r : Fin (N + 2)} (hr : r ≠
   rw [← cells.takeWhile_append_dropWhile (p := fun c ↦ ! decide (r ≤ c.1)),
     List.isChain_append] at valid_move_seq
   have ha := valid_move_seq.2.2
-  simp only [List.head?_eq_head hd', List.getLast?_eq_getLast ht, Option.mem_def,
+  simp only [List.head?_eq_some_head hd', List.getLast?_eq_some_getLast ht, Option.mem_def,
     Option.some.injEq, forall_eq'] at ha
   nth_rw 1 [← cells.takeWhile_append_dropWhile (p := fun c ↦ ! decide (r ≤ c.1))]
   refine List.mem_append_left _ ?_

Archive/MiuLanguage/Basic.lean

@@ -132,7 +132,7 @@ def lcharToMiustr : List Char → Miustr
     | _ => []
 
 instance stringCoeMiustr : Coe String Miustr :=
-  ⟨fun st => lcharToMiustr st.data⟩
+  ⟨fun st => lcharToMiustr st.toList⟩
 
 /-!
 ### Derivability

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -114,15 +114,17 @@ theorem counted_succ_succ (p q : ℕ) :
     obtain ⟨hl₀, hl₁, hl₂⟩ := hl
     obtain hlast | hlast := hl₂ (l.head hlnil) (List.head_mem hlnil)
     · refine Or.inl ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩
-      · rw [List.count_tail, hl₀, List.head?_eq_head hlnil, hlast, beq_self_eq_true, if_pos rfl,
-          Nat.add_sub_cancel]
-      · rw [List.count_tail, hl₁, List.head?_eq_head hlnil, hlast, if_neg (by decide), Nat.sub_zero]
+      · rw [List.count_tail, hl₀, List.head?_eq_some_head hlnil, hlast, beq_self_eq_true,
+          if_pos rfl, Nat.add_sub_cancel]
+      · rw [List.count_tail, hl₁, List.head?_eq_some_head hlnil, hlast, if_neg (by decide),
+          Nat.sub_zero]
       · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
       · rw [← hlast, List.cons_head_tail]
     · refine Or.inr ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩
-      · rw [List.count_tail, hl₀, List.head?_eq_head hlnil, hlast, if_neg (by decide), Nat.sub_zero]
-      · rw [List.count_tail, hl₁, List.head?_eq_head hlnil, hlast, beq_self_eq_true, if_pos rfl,
-          Nat.add_sub_cancel]
+      · rw [List.count_tail, hl₀, List.head?_eq_some_head hlnil, hlast, if_neg (by decide),
+          Nat.sub_zero]
+      · rw [List.count_tail, hl₁, List.head?_eq_some_head hlnil, hlast, beq_self_eq_true,
+          if_pos rfl, Nat.add_sub_cancel]
       · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
       · rw [← hlast, List.cons_head_tail]
   · rintro (⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩ | ⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩)

Cache/Requests.lean

@@ -31,7 +31,7 @@ def extractRepoFromUrl (url : String) : Option String := do
   let url := url.stripSuffix ".git"
   let pos ← url.revFind (· == '/')
   let pos ← url.revFindAux (fun c => c == '/'  || c == ':') pos
-  return (String.Pos.Raw.extract url) (String.Pos.Raw.next url pos) url.endPos
+  return (String.Pos.Raw.extract url) (String.Pos.Raw.next url pos) url.rawEndPos
 
 /-- Spot check if a URL is valid for a git remote -/
 def isRemoteURL (url : String) : Bool :=

Counterexamples/PolynomialIsDomain.lean

@@ -39,7 +39,10 @@ instance : AddCommSemigroup NatMaxAdd where
 
 instance : AddZeroClass NatMaxAdd where
   zero := mk 0
-  zero_add _ := mk.symm.injective (bot_sup_eq _)
+  zero_add _ :=
+    #adaptation_note
+    /-- Prior to nightly-2025-11-03, `mk.symm _` in the next line was just `_`. -/
+    mk.symm.injective (bot_sup_eq (mk.symm _))
   add_zero _ := mk.symm.injective (sup_bot_eq _)
 
 instance : CommMonoidWithZero NatMaxAdd := mk.symm.commMonoidWithZero

Mathlib.lean

@@ -3677,6 +3677,7 @@ import Mathlib.Data.Rat.Cardinal
 import Mathlib.Data.Rat.Cast.CharZero
 import Mathlib.Data.Rat.Cast.Defs
 import Mathlib.Data.Rat.Cast.Lemmas
+import Mathlib.Data.Rat.Cast.OfScientific
 import Mathlib.Data.Rat.Cast.Order
 import Mathlib.Data.Rat.Defs
 import Mathlib.Data.Rat.Denumerable

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -494,7 +494,7 @@ theorem coe_codRestrict (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ x, f x 
 
 theorem injective_codRestrict (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ x : A, f x ∈ S) :
     Function.Injective (NonUnitalAlgHom.codRestrict f S hf) ↔ Function.Injective f :=
-  ⟨fun H _x _y hxy => H <| Subtype.eq hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩
+  ⟨fun H _x _y hxy => H <| Subtype.ext hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩
 
 /-- Restrict the codomain of an `NonUnitalAlgHom` `f` to `f.range`.
 

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -315,8 +315,8 @@ instance (priority := 500) algebra' [CommSemiring R'] [SMul R' R] [Algebra R' A]
     rw [Algebra.algebraMap_eq_smul_one, ← smul_one_smul R x (1 : A), ←
       Algebra.algebraMap_eq_smul_one]
     exact algebraMap_mem S _
-  commutes' := fun _ _ => Subtype.eq <| Algebra.commutes _ _
-  smul_def' := fun _ _ => Subtype.eq <| Algebra.smul_def _ _
+  commutes' := fun _ _ => Subtype.ext <| Algebra.commutes _ _
+  smul_def' := fun _ _ => Subtype.ext <| Algebra.smul_def _ _
 
 instance algebra : Algebra R S := S.algebra'
 
@@ -543,7 +543,7 @@ theorem range_comp_le_range (f : A →ₐ[R] B) (g : B →ₐ[R] C) : (g.comp f)
 
 /-- Restrict the codomain of an algebra homomorphism. -/
 def codRestrict (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ x, f x ∈ S) : A →ₐ[R] S :=
-  { RingHom.codRestrict (f : A →+* B) S hf with commutes' := fun r => Subtype.eq <| f.commutes r }
+  { RingHom.codRestrict (f : A →+* B) S hf with commutes' := fun r => Subtype.ext <| f.commutes r }
 
 @[simp]
 theorem val_comp_codRestrict (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ x, f x ∈ S) :
@@ -557,7 +557,7 @@ theorem coe_codRestrict (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ x, f
 
 theorem injective_codRestrict (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ x, f x ∈ S) :
     Function.Injective (f.codRestrict S hf) ↔ Function.Injective f :=
-  ⟨fun H _x _y hxy => H <| Subtype.eq hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩
+  ⟨fun H _x _y hxy => H <| Subtype.ext hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩
 
 /-- Restrict the codomain of an `AlgHom` `f` to `f.range`.
 

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -281,7 +281,7 @@ noncomputable def botEquivOfInjective (h : Function.Injective (algebraMap R A))
     (⊥ : Subalgebra R A) ≃ₐ[R] R :=
   AlgEquiv.symm <|
     AlgEquiv.ofBijective (Algebra.ofId R _)
-      ⟨fun _x _y hxy => h (congr_arg Subtype.val hxy :), fun ⟨_y, x, hx⟩ => ⟨x, Subtype.eq hx⟩⟩
+      ⟨fun _x _y hxy => h (congr_arg Subtype.val hxy :), fun ⟨_y, x, hx⟩ => ⟨x, Subtype.ext hx⟩⟩
 
 /-- The bottom subalgebra is isomorphic to the field. -/
 @[simps! symm_apply]

Mathlib/Algebra/BigOperators/Fin.lean

@@ -464,7 +464,7 @@ theorem partialProd_zero (f : Fin n → M) : partialProd f 0 = 1 := by simp [par
 @[to_additive]
 theorem partialProd_succ (f : Fin n → M) (j : Fin n) :
     partialProd f j.succ = partialProd f (Fin.castSucc j) * f j := by
-  simp [partialProd, List.take_succ]
+  simp [partialProd, List.take_add_one]
 
 @[to_additive]
 theorem partialProd_succ' (f : Fin (n + 1) → M) (j : Fin (n + 1)) :
@@ -505,11 +505,11 @@ lemma partialProd_contractNth {G : Type*} [Monoid G] {n : ℕ}
       simp only [lt_def, coe_castSucc, val_succ] <;>
       omega
     · rw [succAbove_of_castSucc_lt, contractNth_apply_of_eq _ _ _ _ h,
-        succAbove_of_le_castSucc, castSucc_fin_succ, partialProd_succ, mul_assoc] <;>
+        succAbove_of_le_castSucc, castSucc_succ, partialProd_succ, mul_assoc] <;>
       simp only [castSucc_lt_succ_iff, le_def, coe_castSucc] <;>
       omega
     · rw [succAbove_of_le_castSucc, succAbove_of_le_castSucc, contractNth_apply_of_gt _ _ _ _ h,
-        castSucc_fin_succ] <;>
+        castSucc_succ] <;>
       simp only [le_def, val_succ, coe_castSucc] <;>
       omega
 
@@ -535,13 +535,13 @@ theorem inv_partialProd_mul_eq_contractNth {G : Type*} [Group G] (g : Fin (n + 1
     · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
       exact le_of_lt h
   · rwa [succAbove_of_castSucc_lt, succAbove_of_le_castSucc, partialProd_succ,
-    castSucc_fin_succ, ← mul_assoc,
+    castSucc_succ, ← mul_assoc,
       partialProd_right_inv, contractNth_apply_of_eq]
     · simp [le_iff_val_le_val, ← h]
     · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
       exact le_of_eq h
   · rwa [succAbove_of_le_castSucc, succAbove_of_le_castSucc, partialProd_succ, partialProd_succ,
-      castSucc_fin_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
+      castSucc_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
     · exact le_iff_val_le_val.2 (le_of_lt h)
     · rw [le_iff_val_le_val, val_succ]
       exact Nat.succ_le_of_lt h

Mathlib/Algebra/BigOperators/Ring/Finset.lean

@@ -140,7 +140,7 @@ lemma prod_sum {κ : ι → Type*} (s : Finset ι) (t : ∀ i, Finset (κ i)) (f
       congr with ⟨v, hv⟩
       congr
       exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
-    · exact fun _ _ _ _ => Subtype.eq ∘ Subtype.mk.inj
+    · exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj
     · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
         Subtype.exists, exists_prop, exists_eq_right] using ha
 

Mathlib/Algebra/Category/Ring/Constructions.lean

@@ -346,7 +346,7 @@ instance : IsLocalHom (equalizerFork f g).ι.hom := by
     conv_rhs => rw [h₁]
     rw [← f.hom.map_mul, ← g.hom.map_mul, h₄, f.hom.map_one, g.hom.map_one]
   rw [isUnit_iff_exists_inv]
-  exact ⟨⟨y, this⟩, Subtype.eq h₃⟩
+  exact ⟨⟨y, this⟩, Subtype.ext h₃⟩
 
 @[instance]
 theorem equalizer_ι_isLocalHom (F : WalkingParallelPair ⥤ CommRingCat.{u}) :

Mathlib/Algebra/CharP/Subring.lean

@@ -19,14 +19,14 @@ instance subsemiring (R : Type u) [Semiring R] (p : ℕ) [CharP R p] (S : Subsem
   ⟨fun x =>
     Iff.symm <|
       (CharP.cast_eq_zero_iff R p x).symm.trans
-        ⟨fun h => Subtype.eq <| show S.subtype x = 0 by rw [map_natCast, h], fun h =>
+        ⟨fun h => Subtype.ext <| show S.subtype x = 0 by rw [map_natCast, h], fun h =>
           map_natCast S.subtype x ▸ by rw [h, RingHom.map_zero]⟩⟩
 
 instance subring (R : Type u) [Ring R] (p : ℕ) [CharP R p] (S : Subring R) : CharP S p :=
   ⟨fun x =>
     Iff.symm <|
       (CharP.cast_eq_zero_iff R p x).symm.trans
-        ⟨fun h => Subtype.eq <| show S.subtype x = 0 by rw [map_natCast, h], fun h =>
+        ⟨fun h => Subtype.ext <| show S.subtype x = 0 by rw [map_natCast, h], fun h =>
           map_natCast S.subtype x ▸ by rw [h, RingHom.map_zero]⟩⟩
 
 instance subring' (R : Type u) [CommRing R] (p : ℕ) [CharP R p] (S : Subring R) : CharP S p :=

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -230,7 +230,8 @@ theorem fib_le_of_contsAux_b :
           mt (terminated_stable (n - 1).pred_le) not_terminatedAt_pred_n
         -- use the IH to get the inequalities for `pconts` and `ppconts`
         have ppred_nth_fib_le_ppconts_B : (fib n : K) ≤ ppconts.b :=
-          IH n (lt_trans (Nat.lt.base n) <| Nat.lt.base <| n + 1) (Or.inr not_terminatedAt_ppred_n)
+          IH n (lt_trans (Nat.lt_add_one n) <| Nat.lt_add_one <| n + 1)
+            (Or.inr not_terminatedAt_ppred_n)
         suffices (fib (n + 1) : K) ≤ gp.b * pconts.b by gcongr
         -- finally use the fact that `1 ≤ gp.b` to solve the goal
         suffices 1 * (fib (n + 1) : K) ≤ gp.b * pconts.b by rwa [one_mul] at this

Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean

@@ -330,7 +330,7 @@ theorem convs_eq_convs' [Field K] [LinearOrder K] [IsStrictOrderedRing K]
     · have g'_eq_g : g' = g := squashGCF_eq_self_of_terminated terminatedAt_n
       rw [convs_stable_of_terminated n.le_succ terminatedAt_n, g'_eq_g, IH _]
       intro _ _ m_lt_n s_mth_eq
-      exact s_pos (Nat.lt.step m_lt_n) s_mth_eq
+      exact s_pos (Nat.lt_succ_of_lt m_lt_n) s_mth_eq
     · suffices g.convs (n + 1) = g'.convs n by
         -- invoke the IH for the squashed gcf
         rwa [← IH]
@@ -349,12 +349,12 @@ theorem convs_eq_convs' [Field K] [LinearOrder K] [IsStrictOrderedRing K]
               squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
             grind
           have m_lt_n : m < m.succ := Nat.lt_succ_self m
-          refine ⟨(s_pos (Nat.lt.step m_lt_n) mth_s_eq).left, ?_⟩
-          refine add_pos (s_pos (Nat.lt.step m_lt_n) mth_s_eq).right ?_
+          refine ⟨(s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).left, ?_⟩
+          refine add_pos (s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).right ?_
           have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
           exact div_pos this.left this.right
         · -- the easy case: before the squashed position, nothing changes
-          refine s_pos (Nat.lt.step <| Nat.lt.step succ_m_lt_n) ?_
+          refine s_pos (Nat.lt_succ_of_lt <| Nat.lt_succ_of_lt succ_m_lt_n) ?_
           exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'
       -- now the result follows from the fact that the convergents coincide at the squashed position
       -- as established in `succ_nth_conv_eq_squashGCF_nth_conv`.

Mathlib/Algebra/DirectSum/Internal.lean

@@ -72,7 +72,7 @@ theorem SetLike.natCast_mem_graded [Zero ι] [AddMonoidWithOne R] [SetLike σ R]
 theorem SetLike.intCast_mem_graded [Zero ι] [AddGroupWithOne R] [SetLike σ R]
     [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedOne A] (z : ℤ) : (z : R) ∈ A 0 := by
   cases z
-  · rw [Int.ofNat_eq_coe, Int.cast_natCast]
+  · rw [Int.ofNat_eq_natCast, Int.cast_natCast]
     exact SetLike.natCast_mem_graded _ _
   · rw [Int.cast_negSucc]
     exact neg_mem (SetLike.natCast_mem_graded _ _)

Mathlib/Algebra/Group/Fin/Basic.lean

@@ -118,7 +118,7 @@ lemma lt_sub_iff {n : ℕ} {a b : Fin n} : a < a - b ↔ a < b := by
       Nat.mod_eq_of_lt, Nat.sub_add_cancel b.is_lt.le] using
         (le_trans (mod_le _ _) (le_add_left _ _))
   · intro h
-    rw [lt_iff_val_lt_val, sub_def]
+    rw [lt_def, sub_def]
     simp only
     obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt b.is_lt
     have : n + 1 - b = k + 1 := by
@@ -133,7 +133,7 @@ lemma sub_le_iff {n : ℕ} {a b : Fin n} : a - b ≤ a ↔ b ≤ a := by
 
 @[simp]
 lemma lt_one_iff {n : ℕ} (x : Fin (n + 2)) : x < 1 ↔ x = 0 := by
-  simp [lt_iff_val_lt_val]
+  simp [lt_def]
 
 lemma lt_sub_one_iff {k : Fin (n + 2)} : k < k - 1 ↔ k = 0 := by
   simp

Mathlib/Algebra/Group/Int/Even.lean

@@ -87,7 +87,7 @@ theorem isSquare_sign_iff {z : ℤ} : IsSquare z.sign ↔ 0 ≤ z := by
   | pred =>
     rw [sign_eq_neg_one_of_neg (by cutsat), ← neg_add', Int.neg_nonneg]
     norm_cast
-    simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero, succ_ne_self, and_false, iff_false]
+    simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero_iff, succ_ne_self, and_false, iff_false]
     rintro ⟨a | a, ⟨⟩⟩
 
 end Int

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -210,7 +210,7 @@ open Fintype
 @[to_additive]
 theorem card_bot {_ : Fintype (⊥ : Submonoid M)} : card (⊥ : Submonoid M) = 1 :=
   card_eq_one_iff.2
-    ⟨⟨(1 : M), Set.mem_singleton 1⟩, fun ⟨_y, hy⟩ => Subtype.eq <| mem_bot.1 hy⟩
+    ⟨⟨(1 : M), Set.mem_singleton 1⟩, fun ⟨_y, hy⟩ => Subtype.ext <| mem_bot.1 hy⟩
 
 @[to_additive]
 theorem eq_bot_of_card_le (h : card S ≤ 1) : S = ⊥ :=