chore: bump toolchain to v4.21.0-rc1 (leanprover-community#25384)

Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>

Author: 4 people

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -90,8 +90,9 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
               · simp_all
         · have := ht₃ v
           have := he₃ v
-          simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_eq_eq_not,
-              Bool.not_true, AList.lookup_insert_eq_none, ne_eq, AList.lookup_insert]
+          simp_all? says
+            simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true,
+              AList.lookup_insert_eq_none, ne_eq, AList.lookup_insert, reduceCtorEq, imp_false]
           obtain ⟨⟨⟨tn, tc⟩, tr⟩, td⟩ := ht₂
           split <;> rename_i h'
           · subst h'
@@ -101,9 +102,10 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
           have := he₃ w
           by_cases h : w = v
           · subst h; simp_all
-          · simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_eq_eq_not,
-              Bool.not_true, AList.lookup_insert_eq_none, ne_eq, not_false_eq_true,
-              AList.lookup_insert_ne, implies_true]
+          · simp_all? says
+              simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true,
+                AList.lookup_insert_eq_none, ne_eq, not_false_eq_true, AList.lookup_insert_ne,
+                implies_true]
             obtain ⟨⟨⟨en, ec⟩, er⟩, ed⟩ := he₂
             split at b <;> rename_i h'
             · subst h'; simp_all

Archive/Imo/Imo2015Q6.lean

@@ -179,7 +179,7 @@ theorem result (ha : Condition a) :
     ∃ b > 0, ∃ N, ∀ m ≥ N, ∀ n > m, |∑ j ∈ Ico m n, (a j - b)| ≤ 1007 ^ 2 := by
   obtain ⟨b, N, hbN⟩ := exists_max_card_pool ha
   have bp := b_pos ha hbN
-  use b, Int.ofNat_pos.mpr bp, N; intro m hm n hn; rw [sum_telescope ha hbN hm hn]
+  use b, Int.natCast_pos.mpr bp, N; intro m hm n hn; rw [sum_telescope ha hbN hm hn]
   calc
     _ ≤ ∑ i ∈ range (b - 1), (2014 - i : ℤ) - ∑ i ∈ range b, (i : ℤ) :=
       abs_sub_le_of_le_of_le (le_sum_pool ha hbN (hm.trans hn.le))

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -115,13 +115,14 @@ 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 hlnil, hl₀, hlast, beq_self_eq_true, if_pos rfl, Nat.add_sub_cancel]
-      · rw [List.count_tail hlnil, hl₁, hlast, if_neg (by decide), Nat.sub_zero]
+      · rw [List.count_tail, hl₀, List.head?_eq_head, hlast, beq_self_eq_true, if_pos rfl,
+          Nat.add_sub_cancel]
+      · rw [List.count_tail, hl₁, List.head?_eq_head, hlast, if_neg (by decide), Nat.sub_zero]
       · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
       · rw [← hlast, List.head_cons_tail]
     · refine Or.inr ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩
-      · rw [List.count_tail hlnil, hl₀, hlast, if_neg (by decide), Nat.sub_zero]
-      · rw [List.count_tail hlnil, hl₁, hlast, beq_self_eq_true, if_pos rfl,
+      · rw [List.count_tail, hl₀, List.head?_eq_head, hlast, if_neg (by decide), Nat.sub_zero]
+      · rw [List.count_tail, hl₁, List.head?_eq_head, 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.head_cons_tail]

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -239,7 +239,7 @@ theorem get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero {ifp_n : IntFract
     (of v).s.get? n = some ⟨1, (IntFractPair.of ifp_n.fr⁻¹).b⟩ :=
   have : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹) := by
     cases ifp_n
-    simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.some_bind,
+    simp only [IntFractPair.stream, Nat.add_eq, add_zero, stream_nth_eq, Option.bind_some,
       ite_eq_right_iff]
     intro; contradiction
   get?_of_eq_some_of_succ_get?_intFractPair_stream this
@@ -253,7 +253,7 @@ theorem of_s_head_aux (v : K) : (of v).s.get? 0 = (IntFractPair.stream v 1).bind
   simp only [of, Stream'.Seq.map_tail, Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.head,
     Stream'.Seq.get?, Stream'.map]
   rw [← Stream'.get_succ, Stream'.get, Option.map.eq_def]
-  split <;> simp_all only [Option.some_bind, Option.none_bind, Function.comp_apply]
+  split <;> simp_all only [Option.bind_some, Option.bind_none, Function.comp_apply]
 
 /-- This gives the first pair of coefficients of the continued fraction of a non-integer `v`.
 -/

Mathlib/Algebra/Field/Rat.lean

@@ -41,7 +41,7 @@ instance instDivisionRing : DivisionRing ℚ := inferInstance
 
 protected lemma inv_nonneg {a : ℚ} (ha : 0 ≤ a) : 0 ≤ a⁻¹ := by
   rw [inv_def']
-  exact divInt_nonneg (Int.ofNat_nonneg a.den) (num_nonneg.mpr ha)
+  exact divInt_nonneg (Int.natCast_nonneg a.den) (num_nonneg.mpr ha)
 
 protected lemma div_nonneg {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b :=
   mul_nonneg ha (Rat.inv_nonneg hb)

Mathlib/Algebra/FreeAlgebra.lean

@@ -349,7 +349,6 @@ private def liftAux (f : X → A) : FreeAlgebra R X →ₐ[R] A where
     rintro ⟨⟩ ⟨⟩
     rfl
   map_zero' := by
-    dsimp
     change algebraMap _ _ _ = _
     simp
   map_add' := by

Mathlib/Algebra/Group/Defs.lean

@@ -327,18 +327,6 @@ section
 
 variable {M : Type u}
 
-/-- The fundamental power operation in a monoid. `npowRec n a = a*a*...*a` n times.
-Use instead `a ^ n`, which has better definitional behavior. -/
-def npowRec [One M] [Mul M] : ℕ → M → M
-  | 0, _ => 1
-  | n + 1, a => npowRec n a * a
-
-/-- The fundamental scalar multiplication in an additive monoid. `nsmulRec n a = a+a+...+a` n
-times. Use instead `n • a`, which has better definitional behavior. -/
-def nsmulRec [Zero M] [Add M] : ℕ → M → M
-  | 0, _ => 0
-  | n + 1, a => nsmulRec n a + a
-
 attribute [to_additive existing] npowRec
 
 variable [One M] [Semigroup M] (m n : ℕ) (hn : n ≠ 0) (a : M) (ha : 1 * a = a)
@@ -445,15 +433,15 @@ where
     k.binaryRec (fun y _ ↦ y) fun bn _n fn y x ↦ fn (cond bn (y * x) y) (x * x)
 
 /--
-A variant of `npowRec` which is a semigroup homomorphisms from `ℕ₊` to `M`.
+A variant of `npowRec` which is a semigroup homomorphism from `ℕ₊` to `M`.
 -/
 def npowRec' {M : Type*} [One M] [Mul M] : ℕ → M → M
   | 0, _ => 1
   | 1, m => m
   | k + 2, m => npowRec' (k + 1) m * m
 
 /--
-A variant of `nsmulRec` which is a semigroup homomorphisms from `ℕ₊` to `M`.
+A variant of `nsmulRec` which is a semigroup homomorphism from `ℕ₊` to `M`.
 -/
 def nsmulRec' {M : Type*} [Zero M] [Add M] : ℕ → M → M
   | 0, _ => 0

Mathlib/Algebra/Group/Fin/Basic.lean

@@ -41,7 +41,7 @@ instance addCommMonoid (n : ℕ) [NeZero n] : AddCommMonoid (Fin n) where
 
 instance instAddMonoidWithOne (n) [NeZero n] : AddMonoidWithOne (Fin n) where
   __ := inferInstanceAs (AddCommMonoid (Fin n))
-  natCast i := Fin.ofNat' n i
+  natCast i := Fin.ofNat n i
   natCast_zero := rfl
   natCast_succ _ := Fin.ext (add_mod _ _ _)
 

Mathlib/Algebra/Homology/AlternatingConst.lean

@@ -35,10 +35,6 @@ def alternatingConst [HasZeroMorphisms C] : C ⥤ ChainComplex C ℕ where
       rintro _ _ i rfl rfl
       by_cases h : Even i <;> simp [Nat.even_add_one, ← Nat.not_even_iff_odd, h] }
   map {X Y} f := { f _ := f }
-  map_id X := by ext; simp
-  map_comp f g := by
-    #adaptation_note /-- Around nightly 2025-03-25, need dsimp only -/
-    dsimp only; ext; simp
 
 variable [HasZeroMorphisms C] [HasZeroObject C]
 

Mathlib/Algebra/Homology/Double.lean

@@ -118,7 +118,6 @@ noncomputable def mkHomFromDouble : double f hi₀₁ ⟶ K where
       eqToHom (by rw [hk₁]) ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom (by rw [hk₁])
     else 0
   comm' k₀ k₁ hk := by
-    dsimp
     by_cases h₀ : k₀ = i₀
     · subst h₀
       rw [dif_pos rfl]