chore: adaptations to nightly-2024-03-11

Archive/MiuLanguage/DecisionSuf.lean

@@ -60,7 +60,7 @@ private theorem der_cons_replicate (n : ℕ) : Derivable (M :: replicate (2 ^ n)
   · -- base case
     constructor
   · -- inductive step
-    rw [succ_eq_add_one, pow_add, pow_one 2, mul_two, replicate_add]
+    rw [pow_add, pow_one 2, mul_two, replicate_add]
     exact Derivable.r2 hk
 
 /-!
@@ -120,7 +120,7 @@ theorem der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append (
     specialize ha (U :: xs)
     intro h₂
     -- We massage the goal into a form amenable to the application of `ha`.
-    rw [succ_eq_add_one, replicate_add, ← append_assoc, ← cons_append, replicate_one, append_assoc,
+    rw [replicate_add, ← append_assoc, ← cons_append, replicate_one, append_assoc,
       singleton_append]
     apply ha
     apply Derivable.r3
@@ -269,7 +269,6 @@ theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count
       · rw [mem_cons, not_or] at hm; exact hm.2
     · -- case `x = U` gives a contradiction.
       exfalso; simp only [count, countP_cons_of_pos (· == U) _ (rfl : U == U)] at hu
-      exact succ_ne_zero _ hu
 set_option linter.uppercaseLean3 false in
 #align miu.count_I_eq_length_of_count_U_zero_and_neg_mem Miu.count_I_eq_length_of_count_U_zero_and_neg_mem
 

Archive/Wiedijk100Theorems/InverseTriangleSum.lean

@@ -33,8 +33,9 @@ theorem Theorem100.inverse_triangle_sum :
   refine' sum_range_induction _ _ (if_pos rfl) _
   rintro (_ | n)
   · rw [if_neg, if_pos] <;> norm_num
-  simp_rw [if_neg (Nat.succ_ne_zero _), Nat.succ_eq_add_one]
-  have A : (n + 1 + 1 : ℚ) ≠ 0 := by norm_cast; norm_num
+  simp only [add_eq_zero, Nat.succ_ne_zero, one_ne_zero, and_self, ↓reduceIte, Nat.cast_add,
+    Nat.cast_succ, Nat.cast_one]
+  have A : (n + 1 + 1 : ℚ) ≠ 0 := by norm_cast
   push_cast
   field_simp
   ring

Archive/Wiedijk100Theorems/Partition.lean

@@ -147,7 +147,7 @@ theorem num_series' [Field α] (i : ℕ) :
       symm
       split_ifs with h
       · suffices
-          ((antidiagonal n.succ).filter fun a : ℕ × ℕ => i + 1 ∣ a.fst ∧ a.snd = i + 1).card =
+          ((antidiagonal (n+1)).filter fun a : ℕ × ℕ => i + 1 ∣ a.fst ∧ a.snd = i + 1).card =
             1 by
           simp only [Set.mem_setOf_eq]; convert congr_arg ((↑) : ℕ → α) this; norm_cast
         rw [card_eq_one]
@@ -164,7 +164,7 @@ theorem num_series' [Field α] (i : ℕ) :
           | 0 => rw [mul_zero] at hp; cases hp
           | p + 1 => rw [hp]; simp [mul_add]
       · suffices
-          (filter (fun a : ℕ × ℕ => i + 1 ∣ a.fst ∧ a.snd = i + 1) (antidiagonal n.succ)).card =
+          (filter (fun a : ℕ × ℕ => i + 1 ∣ a.fst ∧ a.snd = i + 1) (antidiagonal (n+1))).card =
             0 by
           simp only [Set.mem_setOf_eq]; convert congr_arg ((↑) : ℕ → α) this; norm_cast
         rw [card_eq_zero]
@@ -373,7 +373,6 @@ theorem same_gf [Field α] (m : ℕ) :
   rw [partialOddGF, partialDistinctGF]
   induction' m with m ih
   · simp
-  rw [Nat.succ_eq_add_one]
   set! π₀ : PowerSeries α := ∏ i in range m, (1 - X ^ (m + 1 + i + 1)) with hπ₀
   set! π₁ : PowerSeries α := ∏ i in range m, (1 - X ^ (2 * i + 1))⁻¹ with hπ₁
   set! π₂ : PowerSeries α := ∏ i in range m, (1 - X ^ (m + i + 1)) with hπ₂

Counterexamples/CliffordAlgebra_not_injective.lean

@@ -50,10 +50,9 @@ def kIdeal : Ideal (MvPolynomial (Fin 3) (ZMod 2)) :=
 
 theorem mem_kIdeal_iff (x : MvPolynomial (Fin 3) (ZMod 2)) :
     x ∈ kIdeal ↔ ∀ m : Fin 3 →₀ ℕ, m ∈ x.support → ∃ i, 2 ≤ m i := by
-  have :
-      kIdeal = Ideal.span ((monomial · (1 : ZMod 2)) '' Set.range (Finsupp.single · 2)) := by
+  have : kIdeal = Ideal.span ((monomial · (1 : ZMod 2)) '' Set.range (Finsupp.single · 2)) := by
     simp_rw [kIdeal, X, monomial_mul, one_mul, ← Finsupp.single_add, ← Set.range_comp,
-      Function.comp]
+      Function.comp, Nat.reduceAdd]
   rw [this, mem_ideal_span_monomial_image]
   simp
 

Counterexamples/Phillips.lean

@@ -318,7 +318,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
     · have : (s (n + 1)).1 = (s (n + 1)).1 \ (s n).1 ∪ (s n).1 := by
         simpa only [s, Function.iterate_succ', union_diff_self]
           using (diff_union_of_subset <| subset_union_left _ _).symm
-      rw [Nat.succ_eq_add_one, this, f.additive]
+      rw [this, f.additive]
       swap; · exact disjoint_sdiff_self_left
       calc
         ((n + 1 : ℕ) : ℝ) * (ε / 2) = ε / 2 + n * (ε / 2) := by simp only [Nat.cast_succ]; ring

Mathlib/Algebra/BigOperators/Fin.lean

@@ -267,11 +267,10 @@ theorem partialProd_right_inv {G : Type*} [Group G] (f : Fin n → G) (i : Fin n
     specialize hi (lt_trans (Nat.lt_succ_self i) hn)
     simp only [Fin.coe_eq_castSucc, Fin.succ_mk, Fin.castSucc_mk] at hi ⊢
     rw [← Fin.succ_mk _ _ (lt_trans (Nat.lt_succ_self _) hn), ← Fin.succ_mk]
-    rw [Nat.succ_eq_add_one] at hn
     simp only [partialProd_succ, mul_inv_rev, Fin.castSucc_mk]
     -- Porting note: was
     -- assoc_rw [hi, inv_mul_cancel_left]
-    rw [← mul_assoc, mul_left_eq_self, mul_assoc, hi, mul_left_inv]
+    rw [← mul_assoc, mul_left_eq_self, mul_assoc, castSucc_mk, hi, mul_left_inv]
 #align fin.partial_prod_right_inv Fin.partialProd_right_inv
 #align fin.partial_sum_right_neg Fin.partialSum_right_neg
 
@@ -322,19 +321,15 @@ def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
       induction' n with n ih
       · simp
       cases m
-      · dsimp only [Nat.zero_eq] at f -- Porting note: added, wrong zero
-        exact isEmptyElim (f <| Fin.last _)
+      · exact isEmptyElim (f <| Fin.last _)
       simp_rw [Fin.sum_univ_castSucc, Fin.coe_castSucc, Fin.val_last]
       refine' (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq _
-      rw [← one_add_mul (_ : ℕ), add_comm, pow_succ]
-      -- Porting note: added, wrong `succ`
-      rfl⟩)
+      rw [← one_add_mul (_ : ℕ), add_comm, pow_succ]⟩)
     (fun a b => ⟨a / m ^ (b : ℕ) % m, by
       cases' n with n
       · exact b.elim0
       cases' m with m
-      · dsimp only [Nat.zero_eq] at a -- Porting note: added, wrong zero
-        rw [zero_pow n.succ_ne_zero] at a
+      · rw [zero_pow n.succ_ne_zero] at a
         exact a.elim0
       · exact Nat.mod_lt _ m.succ_pos⟩)
     fun a => by
@@ -382,12 +377,9 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
         exact this
       intro n nn f fn
       cases nn
-      · dsimp only [Nat.zero_eq] at fn -- Porting note: added, wrong zero
-        exact isEmptyElim fn
+      · exact isEmptyElim fn
       refine' (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq _
-      rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]
-      -- Porting note: added, wrong `succ`
-      rfl⟩)
+      rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]⟩)
     (fun a b => ⟨(a / ∏ j : Fin b, n (Fin.castLE b.is_lt.le j)) % n b, by
       cases m
       · exact b.elim0

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -363,8 +363,8 @@ def smul : R →+* End ((forget₂ (ModuleCat R) AddCommGroupCat).obj M) where
     { toFun := fun (m : M) => r • m
       map_zero' := by dsimp; rw [smul_zero]
       map_add' := fun x y => by dsimp; rw [smul_add] }
-  map_one' := AddMonoidHom.ext (fun x => by dsimp; rw [one_smul])
-  map_zero' := AddMonoidHom.ext (fun x => by dsimp; rw [zero_smul])
+  map_one' := AddMonoidHom.ext (fun x => by dsimp; rw [one_smul]; rfl)
+  map_zero' := AddMonoidHom.ext (fun x => by dsimp; rw [zero_smul]; rfl)
   map_mul' r s := AddMonoidHom.ext (fun (x : M) => (smul_smul r s x).symm)
   map_add' r s := AddMonoidHom.ext (fun (x : M) => add_smul r s x)
 

Mathlib/Algebra/Category/Ring/Constructions.lean

@@ -147,7 +147,7 @@ section Terminal
 /-- The trivial ring is the (strict) terminal object of `CommRingCat`. -/
 def punitIsTerminal : IsTerminal (CommRingCat.of.{u} PUnit) := by
   refine IsTerminal.ofUnique (h := fun X => ⟨⟨⟨⟨1, rfl⟩, fun _ _ => rfl⟩, ?_, ?_⟩, ?_⟩)
-  · dsimp
+  · rfl
   · intros; dsimp
   · intros f; ext; rfl
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/CharZero/Defs.lean

@@ -84,10 +84,8 @@ theorem cast_ne_zero {n : ℕ} : (n : R) ≠ 0 ↔ n ≠ 0 :=
   not_congr cast_eq_zero
 #align nat.cast_ne_zero Nat.cast_ne_zero
 
-theorem cast_add_one_ne_zero (n : ℕ) : (n + 1 : R) ≠ 0 := by
-  -- Porting note: old proof was `exact_mod_cast n.succ_ne_zero`
-  norm_cast
-  exact n.succ_ne_zero
+theorem cast_add_one_ne_zero (n : ℕ) : (n + 1 : R) ≠ 0 :=
+  mod_cast n.succ_ne_zero
 #align nat.cast_add_one_ne_zero Nat.cast_add_one_ne_zero
 
 @[simp, norm_cast]

Mathlib/Algebra/Function/Support.lean

@@ -115,7 +115,9 @@ theorem disjoint_mulSupport_iff {f : α → M} {s : Set α} :
 
 @[to_additive (attr := simp)]
 theorem mulSupport_eq_empty_iff {f : α → M} : mulSupport f = ∅ ↔ f = 1 := by
-  simp_rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]
+  -- Adaptation note: This used to be `simp_rw` rather than `rw`,
+  -- but this broke `to_additive` as of `nightly-2024-03-07`
+  rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]
   simp
 #align function.mul_support_eq_empty_iff Function.mulSupport_eq_empty_iff
 #align function.support_eq_empty_iff Function.support_eq_empty_iff

Mathlib/Algebra/GeomSum.lean

@@ -442,7 +442,7 @@ theorem Nat.geom_sum_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
 theorem Nat.geom_sum_Ico_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
     ∑ i in Ico 1 n, a / b ^ i ≤ a / (b - 1) := by
   cases' n with n
-  · rw [zero_eq, Ico_eq_empty_of_le (zero_le_one' ℕ), sum_empty]
+  · rw [Ico_eq_empty_of_le (zero_le_one' ℕ), sum_empty]
     exact Nat.zero_le _
   rw [← add_le_add_iff_left a]
   calc

Mathlib/Algebra/Group/NatPowAssoc.lean

@@ -71,7 +71,7 @@ theorem npow_mul_comm (m n : ℕ) (x : M) :
 theorem npow_mul (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ m) ^ n := by
   induction n with
   | zero => rw [npow_zero, Nat.mul_zero, npow_zero]
-  | succ n ih => rw [← Nat.add_one, mul_add, npow_add, ih, mul_one, npow_add, npow_one]
+  | succ n ih => rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
 
 theorem npow_mul' (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ n) ^ m := by
   rw [mul_comm]
@@ -105,7 +105,7 @@ theorem Nat.cast_npow (R : Type*) [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc
     (↑(n ^ m) : R) = (↑n : R) ^ m := by
   induction' m with m ih
   · simp only [pow_zero, Nat.cast_one, npow_zero]
-  · rw [← Nat.add_one, npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
+  · rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
 
 @[simp, norm_cast]
 theorem Int.cast_npow (R : Type*) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R]

Mathlib/Algebra/Homology/Augment.lean

@@ -140,15 +140,15 @@ theorem chainComplex_d_succ_succ_zero (C : ChainComplex V ℕ) (i : ℕ) : C.d (
 def augmentTruncate (C : ChainComplex V ℕ) :
     augment (truncate.obj C) (C.d 1 0) (C.d_comp_d _ _ _) ≅ C where
   hom :=
-    { f := fun i => by cases i <;> exact 𝟙 _
+    { f := fun | 0 => 𝟙 _ | n+1 => 𝟙 _
       comm' := fun i j => by
         -- Porting note: was an rcases n with (_|_|n) but that was causing issues
         match i with
         | 0 | 1 | n+2 =>
           cases' j with j <;> dsimp [augment, truncate] <;> simp
     }
   inv :=
-    { f := fun i => by cases i <;> exact 𝟙 _
+    { f := fun | 0 => 𝟙 _ | n+1 => 𝟙 _
       comm' := fun i j => by
         -- Porting note: was an rcases n with (_|_|n) but that was causing issues
         match i with
@@ -246,10 +246,10 @@ def augment (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d
     rcases j with (_ | _ | j) <;> cases i <;> try simp
     · contradiction
     · rw [C.shape]
+      simp only [Nat.succ_eq_add_one] at s
       simp only [ComplexShape.up_Rel]
       contrapose! s
       rw [← s]
-      rfl
   d_comp_d' i j k hij hjk := by
     rcases k with (_ | _ | k) <;> rcases j with (_ | _ | j) <;> cases i <;> try simp
     cases k
@@ -335,14 +335,14 @@ theorem cochainComplex_d_succ_succ_zero (C : CochainComplex V ℕ) (i : ℕ) : C
 def augmentTruncate (C : CochainComplex V ℕ) :
     augment (truncate.obj C) (C.d 0 1) (C.d_comp_d _ _ _) ≅ C where
   hom :=
-    { f := fun i => by cases i <;> exact 𝟙 _
+    { f := fun | 0 => 𝟙 _ | n+1 => 𝟙 _
       comm' := fun i j => by
         rcases j with (_ | _ | j) <;> cases i <;>
           · dsimp
             -- Porting note (#10959): simp can't handle this now but aesop does
             aesop }
   inv :=
-    { f := fun i => by cases i <;> exact 𝟙 _
+    { f := fun | 0 => 𝟙 _ | n+1 => 𝟙 _
       comm' := fun i j => by
         rcases j with (_ | _ | j) <;> cases' i with i <;>
           · dsimp

Mathlib/Algebra/Homology/ExactSequence.lean

@@ -180,6 +180,12 @@ lemma isComplex₂_mk (S : ComposableArrows C 2) (w : S.map' 0 1 ≫ S.map' 1 2
     S.IsComplex :=
   S.isComplex₂_iff.2 w
 
+-- Adaptation note: nightly-2024-03-11
+-- We turn off simprocs here.
+-- Ideally someone will investigate whether `simp` lemmas can be rearranged
+-- so that this works without the `set_option`,
+-- *or* come up with a proposal regarding finer control of disabling simprocs.
+set_option simprocs false in
 lemma _root_.CategoryTheory.ShortComplex.isComplex_toComposableArrows (S : ShortComplex C) :
     S.toComposableArrows.IsComplex :=
   isComplex₂_mk _ (by simp)

Mathlib/Algebra/Homology/HomologySequence.lean

@@ -110,6 +110,12 @@ instance [K.HasHomology i] [K.HasHomology j] :
   dsimp
   infer_instance
 
+-- Adaptation note: nightly-2024-03-11
+-- We turn off simprocs here.
+-- Ideally someone will investigate whether `simp` lemmas can be rearranged
+-- so that this works without the `set_option`,
+-- *or* come up with a proposal regarding finer control of disabling simprocs.
+set_option simprocs false in
 instance [K.HasHomology i] [K.HasHomology j] :
     Epi ((composableArrows₃ K i j).map' 2 3) := by
   dsimp
@@ -145,6 +151,12 @@ variable (C)
 
 attribute [local simp] homologyMap_comp cyclesMap_comp opcyclesMap_comp
 
+-- Adaptation note: nightly-2024-03-11
+-- We turn off simprocs here.
+-- Ideally someone will investigate whether `simp` lemmas can be rearranged
+-- so that this works without the `set_option`,
+-- *or* come up with a proposal regarding finer control of disabling simprocs.
+set_option simprocs false in
 /-- The functor `HomologicalComplex C c ⥤ ComposableArrows C 3` that maps `K` to the
 diagram `K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j`. -/
 @[simps]

Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean

@@ -87,9 +87,9 @@ noncomputable def mappingConeHomOfDegreewiseSplitXIso (p q : ℤ) (hpq : p + 1 =
     have f_r := (σ (p + 1)).f_r
     dsimp at s_g f_r ⊢
     simp? [mappingCone.ext_from_iff _ (p + 1) _ rfl, reassoc_of% f_r, reassoc_of% s_g] says
-      simp only [Cochain.ofHom_v, id_comp, comp_sub, sub_comp, assoc, reassoc_of% s_g,
-        ShortComplex.Splitting.s_r_assoc, ShortComplex.map_X₃, eval_obj, ShortComplex.map_X₁,
-        zero_comp, comp_zero, reassoc_of% f_r, zero_sub, sub_neg_eq_add,
+      simp only [Cochain.ofHom_v, Int.reduceNeg, id_comp, comp_sub, sub_comp, assoc,
+        reassoc_of% s_g, ShortComplex.Splitting.s_r_assoc, ShortComplex.map_X₃, eval_obj,
+        ShortComplex.map_X₁, zero_comp, comp_zero, reassoc_of% f_r, zero_sub, sub_neg_eq_add,
         mappingCone.ext_from_iff _ (p + 1) _ rfl, comp_add, mappingCone.inl_v_fst_v_assoc,
         mappingCone.inl_v_snd_v_assoc, shiftFunctor_obj_X', sub_zero, add_zero, comp_id,
         mappingCone.inr_f_fst_v_assoc, mappingCone.inr_f_snd_v_assoc, add_left_eq_self, neg_eq_zero,