chore: bump to nightly-2023-07-01 (#5409)

- [x] depends on: leanprover-community/batteries#163
- [x] depends on: #5584
- [x] depends on: #5715
- [x] depends on: #5729
- [x] depends on: leanprover-community/batteries#173

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Archive/Imo/Imo1960Q1.lean

@@ -93,6 +93,7 @@ theorem searchUpTo_end {c} (H : SearchUpTo c 1001) {n : ℕ} (ppn : ProblemPredi
   H.2 _ (by linarith [lt_1000 ppn]) ppn
 #align imo1960_q1.search_up_to_end Imo1960Q1.searchUpTo_end
 
+set_option maxHeartbeats 2000000 in
 theorem right_direction {n : ℕ} : ProblemPredicate n → SolutionPredicate n := by
   have := searchUpTo_start
   iterate 82

Archive/Imo/Imo1962Q1.lean

@@ -134,7 +134,7 @@ Now we combine these cases to show that 153846 is the smallest solution.
 
 
 theorem satisfied_by_153846 : ProblemPredicate 153846 := by
-  dsimp [ProblemPredicate, digits_def', ofDigits]; norm_num
+  dsimp [ProblemPredicate]; norm_num
 #align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846
 
 theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846 := by

Archive/Sensitivity.lean

@@ -106,8 +106,8 @@ theorem succ_n_eq (p q : Q n.succ) : p = q ↔ p 0 = q 0 ∧ π p = π q := by
     ext x
     by_cases hx : x = 0
     · rwa [hx]
-    · rw [← Fin.succ_pred x hx]
-      convert congr_fun h (Fin.pred x hx)
+    · rw [← Fin.succ_pred x <| Fin.vne_of_ne hx]
+      convert congr_fun h (Fin.pred x <| Fin.vne_of_ne hx)
 #align sensitivity.Q.succ_n_eq Sensitivity.Q.succ_n_eq
 
 /-- The adjacency relation defining the graph structure on `Q n`:
@@ -131,7 +131,7 @@ theorem adj_iff_proj_eq {p q : Q n.succ} (h₀ : p 0 ≠ q 0) : q ∈ p.adjacent
     use 0, h₀
     intro y hy
     contrapose! hy
-    rw [← Fin.succ_pred _ hy]
+    rw [← Fin.succ_pred _ <| Fin.vne_of_ne hy]
     apply congr_fun heq
 #align sensitivity.Q.adj_iff_proj_eq Sensitivity.Q.adj_iff_proj_eq
 
@@ -142,14 +142,15 @@ theorem adj_iff_proj_adj {p q : Q n.succ} (h₀ : p 0 = q 0) :
   constructor
   · rintro ⟨i, h_eq, h_uni⟩
     have h_i : i ≠ 0 := fun h_i => absurd h₀ (by rwa [h_i] at h_eq )
-    use i.pred h_i,
+    use i.pred <| Fin.vne_of_ne h_i,
       show p (Fin.succ (Fin.pred i _)) ≠ q (Fin.succ (Fin.pred i _)) by rwa [Fin.succ_pred]
     intro y hy
     simp [Eq.symm (h_uni _ hy)]
   · rintro ⟨i, h_eq, h_uni⟩
     use i.succ, h_eq
     intro y hy
-    rw [← Fin.pred_inj (ha := ?ha) (hb := ?hb), Fin.pred_succ]
+    rw [← Fin.pred_inj (ha := Fin.vne_of_ne (?ha : y ≠ 0)) (hb := Fin.vne_of_ne (?hb : i.succ ≠ 0)),
+      Fin.pred_succ]
     case ha =>
       contrapose! hy
       rw [hy, h₀]
@@ -233,8 +234,8 @@ theorem epsilon_total {v : V n} (h : ∀ p : Q n, (ε p) v = 0) : v = 0 := by
   · dsimp [ε] at h; exact h fun _ => true
   · cases' v with v₁ v₂
     ext <;> change _ = (0 : V n) <;> simp only <;> apply ih <;> intro p <;>
-      [let q : Q n.succ := fun i => if h : i = 0 then true else p (i.pred h);
-      let q : Q n.succ := fun i => if h : i = 0 then false else p (i.pred h)]
+      [let q : Q n.succ := fun i => if h : i = 0 then true else p (i.pred <| Fin.vne_of_ne h);
+      let q : Q n.succ := fun i => if h : i = 0 then false else p (i.pred <| Fin.vne_of_ne h)]
     all_goals
       specialize h q
       first

Counterexamples/MapFloor.lean

@@ -88,7 +88,7 @@ theorem pos_iff {p : ℤ[ε]} : 0 < p ↔ 0 < p.trailingCoeff := by
 instance : LinearOrderedCommRing ℤ[ε] :=
   { IntWithEpsilon.linearOrder, IntWithEpsilon.commRing, IntWithEpsilon.orderedAddCommGroup,
     IntWithEpsilon.nontrivial with
-    zero_le_one := Or.inr ⟨0, by simp; rw [coeff_zero, coeff_one_zero]; linarith⟩
+    zero_le_one := Or.inr ⟨0, by simp⟩
     mul_pos := fun p q => by simp_rw [pos_iff]; rw [trailingCoeff_mul]; exact mul_pos}
 
 instance : FloorRing ℤ[ε] :=

Mathlib/Algebra/Algebra/Basic.lean

@@ -344,10 +344,8 @@ instance (priority := 200) toModule : Module R A where
   zero_smul := by simp [smul_def']
 #align algebra.to_module Algebra.toModule
 
--- From now on, we don't want to use the following instance anymore.
--- Unfortunately, leaving it in place caused deterministic timeouts later in mathlib3.
--- porting note: todo: is it still required in Mathlib 4?
-attribute [instance 0] Algebra.toSMul
+-- porting note: this caused deterministic timeouts later in mathlib3 but not in mathlib 4.
+-- attribute [instance 0] Algebra.toSMul
 
 theorem smul_def (r : R) (x : A) : r • x = algebraMap R A r * x :=
   Algebra.smul_def' r x

Mathlib/Algebra/BigOperators/Fin.lean

@@ -18,7 +18,7 @@ import Mathlib.Logic.Equiv.Fin
 
 Some results about products and sums over the type `Fin`.
 
-The most important results are the induction formulas `Fin.prod_univ_castSuccEmb`
+The most important results are the induction formulas `Fin.prod_univ_castSucc`
 and `Fin.prod_univ_succ`, and the formula `Fin.prod_const` for the product of a
 constant function. These results have variants for sums instead of products.
 
@@ -71,8 +71,9 @@ is the product of `f x`, for some `x : Fin (n + 1)` times the remaining product
 `f x`, for some `x : Fin (n + 1)` plus the remaining product"]
 theorem prod_univ_succAbove [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) (x : Fin (n + 1)) :
     ∏ i, f i = f x * ∏ i : Fin n, f (x.succAbove i) := by
-  rw [univ_succAbove, prod_cons, Finset.prod_map _ x.succAbove.toEmbedding,
+  rw [univ_succAbove, prod_cons, Finset.prod_map _ x.succAboveEmb.toEmbedding,
     RelEmbedding.coe_toEmbedding]
+  rfl
 #align fin.prod_univ_succ_above Fin.prod_univ_succAbove
 #align fin.sum_univ_succ_above Fin.sum_univ_succAbove
 
@@ -90,11 +91,11 @@ theorem prod_univ_succ [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
 is the product of `f (Fin.last n)` plus the remaining product -/
 @[to_additive "A sum of a function `f : Fin (n + 1) → β` over all `Fin (n + 1)` is the sum of
 `f (Fin.last n)` plus the remaining sum"]
-theorem prod_univ_castSuccEmb [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
-    ∏ i, f i = (∏ i : Fin n, f (Fin.castSuccEmb i)) * f (last n) := by
+theorem prod_univ_castSucc [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
+    ∏ i, f i = (∏ i : Fin n, f (Fin.castSucc i)) * f (last n) := by
   simpa [mul_comm] using prod_univ_succAbove f (last n)
-#align fin.prod_univ_cast_succ Fin.prod_univ_castSuccEmb
-#align fin.sum_univ_cast_succ Fin.sum_univ_castSuccEmb
+#align fin.prod_univ_cast_succ Fin.prod_univ_castSucc
+#align fin.sum_univ_cast_succ Fin.sum_univ_castSucc
 
 @[to_additive]
 theorem prod_cons [CommMonoid β] {n : ℕ} (x : β) (f : Fin n → β) :
@@ -116,46 +117,46 @@ theorem prod_univ_two [CommMonoid β] (f : Fin 2 → β) : ∏ i, f i = f 0 * f
 
 @[to_additive]
 theorem prod_univ_three [CommMonoid β] (f : Fin 3 → β) : ∏ i, f i = f 0 * f 1 * f 2 := by
-  rw [prod_univ_castSuccEmb, prod_univ_two]
+  rw [prod_univ_castSucc, prod_univ_two]
   rfl
 #align fin.prod_univ_three Fin.prod_univ_three
 #align fin.sum_univ_three Fin.sum_univ_three
 
 @[to_additive]
 theorem prod_univ_four [CommMonoid β] (f : Fin 4 → β) : ∏ i, f i = f 0 * f 1 * f 2 * f 3 := by
-  rw [prod_univ_castSuccEmb, prod_univ_three]
+  rw [prod_univ_castSucc, prod_univ_three]
   rfl
 #align fin.prod_univ_four Fin.prod_univ_four
 #align fin.sum_univ_four Fin.sum_univ_four
 
 @[to_additive]
 theorem prod_univ_five [CommMonoid β] (f : Fin 5 → β) :
     ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 := by
-  rw [prod_univ_castSuccEmb, prod_univ_four]
+  rw [prod_univ_castSucc, prod_univ_four]
   rfl
 #align fin.prod_univ_five Fin.prod_univ_five
 #align fin.sum_univ_five Fin.sum_univ_five
 
 @[to_additive]
 theorem prod_univ_six [CommMonoid β] (f : Fin 6 → β) :
     ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 := by
-  rw [prod_univ_castSuccEmb, prod_univ_five]
+  rw [prod_univ_castSucc, prod_univ_five]
   rfl
 #align fin.prod_univ_six Fin.prod_univ_six
 #align fin.sum_univ_six Fin.sum_univ_six
 
 @[to_additive]
 theorem prod_univ_seven [CommMonoid β] (f : Fin 7 → β) :
     ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 := by
-  rw [prod_univ_castSuccEmb, prod_univ_six]
+  rw [prod_univ_castSucc, prod_univ_six]
   rfl
 #align fin.prod_univ_seven Fin.prod_univ_seven
 #align fin.sum_univ_seven Fin.sum_univ_seven
 
 @[to_additive]
 theorem prod_univ_eight [CommMonoid β] (f : Fin 8 → β) :
     ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7 := by
-  rw [prod_univ_castSuccEmb, prod_univ_seven]
+  rw [prod_univ_castSucc, prod_univ_seven]
   rfl
 #align fin.prod_univ_eight Fin.prod_univ_eight
 #align fin.sum_univ_eight Fin.sum_univ_eight
@@ -231,7 +232,7 @@ theorem partialProd_zero (f : Fin n → α) : partialProd f 0 = 1 := by simp [pa
 
 @[to_additive]
 theorem partialProd_succ (f : Fin n → α) (j : Fin n) :
-    partialProd f j.succ = partialProd f (Fin.castSuccEmb j) * f j := by
+    partialProd f j.succ = partialProd f (Fin.castSucc j) * f j := by
   simp [partialProd, List.take_succ, List.ofFnNthVal, dif_pos j.is_lt, ← Option.coe_def]
 #align fin.partial_prod_succ Fin.partialProd_succ
 #align fin.partial_sum_succ Fin.partialSum_succ
@@ -248,23 +249,23 @@ theorem partialProd_succ' (f : Fin (n + 1) → α) (j : Fin (n + 1)) :
 theorem partialProd_left_inv {G : Type _} [Group G] (f : Fin (n + 1) → G) :
     (f 0 • partialProd fun i : Fin n => (f i)⁻¹ * f i.succ) = f :=
   funext fun x => Fin.inductionOn x (by simp) fun x hx => by
-    simp only [coe_eq_castSuccEmb, Pi.smul_apply, smul_eq_mul] at hx ⊢
+    simp only [coe_eq_castSucc, Pi.smul_apply, smul_eq_mul] at hx ⊢
     rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]
 #align fin.partial_prod_left_inv Fin.partialProd_left_inv
 #align fin.partial_sum_left_neg Fin.partialSum_left_neg
 
 @[to_additive]
 theorem partialProd_right_inv {G : Type _} [Group G] (f : Fin n → G) (i : Fin n) :
-    (partialProd f (Fin.castSuccEmb i))⁻¹ * partialProd f i.succ = f i := by
+    (partialProd f (Fin.castSucc i))⁻¹ * partialProd f i.succ = f i := by
   cases' i with i hn
   induction i with
   | zero => simp [-Fin.succ_mk, partialProd_succ]
   | succ i hi =>
     specialize hi (lt_trans (Nat.lt_succ_self i) hn)
-    simp only [Fin.coe_eq_castSuccEmb, Fin.succ_mk, Fin.castSuccEmb_mk] at hi ⊢
+    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.castSuccEmb_mk]
+    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]
@@ -284,20 +285,20 @@ Useful for defining group cohomology. -/
       Useful for defining group cohomology."]
 theorem inv_partialProd_mul_eq_contractNth {G : Type _} [Group G] (g : Fin (n + 1) → G)
     (j : Fin (n + 1)) (k : Fin n) :
-    (partialProd g (j.succ.succAbove (Fin.castSuccEmb k)))⁻¹ * partialProd g (j.succAbove k).succ =
+    (partialProd g (j.succ.succAbove (Fin.castSucc k)))⁻¹ * partialProd g (j.succAbove k).succ =
       j.contractNth (· * ·) g k := by
   rcases lt_trichotomy (k : ℕ) j with (h | h | h)
   · rwa [succAbove_below, succAbove_below, partialProd_right_inv, contractNth_apply_of_lt]
     · assumption
-    · rw [castSuccEmb_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
+    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
       exact le_of_lt h
-  · rwa [succAbove_below, succAbove_above, partialProd_succ, castSuccEmb_fin_succ, ← mul_assoc,
+  · rwa [succAbove_below, succAbove_above, partialProd_succ, castSucc_fin_succ, ← mul_assoc,
       partialProd_right_inv, contractNth_apply_of_eq]
     · simp [le_iff_val_le_val, ← h]
-    · rw [castSuccEmb_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
+    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
       exact le_of_eq h
   · rwa [succAbove_above, succAbove_above, partialProd_succ, partialProd_succ,
-      castSuccEmb_fin_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
+      castSucc_fin_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
@@ -318,7 +319,7 @@ def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
       cases m
       · dsimp only [Nat.zero_eq] at f -- porting note: added, wrong zero
         exact isEmptyElim (f <| Fin.last _)
-      simp_rw [Fin.sum_univ_castSuccEmb, Fin.coe_castSuccEmb, Fin.val_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`
@@ -364,15 +365,15 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
     (fun f => ⟨∑ i, f i * ∏ j, n (Fin.castLE i.is_lt.le j), by
       induction' m with m ih
       · simp
-      rw [Fin.prod_univ_castSuccEmb, Fin.sum_univ_castSuccEmb]
+      rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
       suffices
         ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
           ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
             (∏ i : Fin m, n i) * nn by
         replace := this (Fin.init n) (n (Fin.last _)) (Fin.init f) (f (Fin.last _))
         rw [← Fin.snoc_init_self f]
         simp (config := { singlePass := true }) only [← Fin.snoc_init_self n]
-        simp_rw [Fin.snoc_castSuccEmb, Fin.snoc_last, Fin.snoc_init_self n]
+        simp_rw [Fin.snoc_castSucc, Fin.snoc_last, Fin.snoc_init_self n]
         exact this
       intro n nn f fn
       cases nn

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -419,7 +419,7 @@ def kernelIsoKer {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
     { toFun := fun g => ⟨kernel.ι f g, FunLike.congr_fun (kernel.condition f) g⟩
       map_zero' := by
         refine Subtype.ext ?_
-        simpa using (AddSubgroup.coe_zero _).symm
+        simp [(AddSubgroup.coe_zero _).symm]
       map_add' := fun g g' => by
         refine Subtype.ext ?_
         change _ = _ + _

Mathlib/Algebra/CharP/Basic.lean

@@ -587,7 +587,6 @@ instance (priority := 100) CharOne.subsingleton [CharP R 1] : Subsingleton R :=
       _ = 0 * r := by rw [CharP.cast_eq_zero]
       _ = 0 := by rw [MulZeroClass.zero_mul]
 
-
 theorem false_of_nontrivial_of_char_one [Nontrivial R] [CharP R 1] : False :=
   false_of_nontrivial_of_subsingleton R
 #align char_p.false_of_nontrivial_of_char_one CharP.false_of_nontrivial_of_char_one

Mathlib/Algebra/CharZero/Defs.lean

@@ -103,21 +103,21 @@ namespace OfNat
 
 variable [AddMonoidWithOne R] [CharZero R]
 
-@[simp] lemma ofNat_ne_zero (n : ℕ) [h : n.AtLeastTwo] : (ofNat n : R) ≠ 0 :=
+@[simp] lemma ofNat_ne_zero (n : ℕ) [h : n.AtLeastTwo] : (no_index (ofNat n) : R) ≠ 0 :=
   Nat.cast_ne_zero.2 <| ne_of_gt <| lt_trans Nat.one_pos h.prop
 
-@[simp] lemma zero_ne_ofNat (n : ℕ) [n.AtLeastTwo] : 0 ≠ (ofNat n : R) :=
+@[simp] lemma zero_ne_ofNat (n : ℕ) [n.AtLeastTwo] : 0 ≠ (no_index (ofNat n) : R) :=
   (ofNat_ne_zero n).symm
 
-@[simp] lemma ofNat_ne_one (n : ℕ) [h : n.AtLeastTwo] : (ofNat n : R) ≠ 1 := by
+@[simp] lemma ofNat_ne_one (n : ℕ) [h : n.AtLeastTwo] : (no_index (ofNat n) : R) ≠ 1 := by
   rw [← Nat.cast_eq_ofNat, ← @Nat.cast_one R, Ne.def, Nat.cast_inj]
   exact ne_of_gt h.prop
 
-@[simp] lemma one_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (1 : R) ≠ ofNat n :=
+@[simp] lemma one_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (1 : R) ≠ no_index (ofNat n) :=
   (ofNat_ne_one n).symm
 
 @[simp] lemma ofNat_eq_ofNat {m n : ℕ} [m.AtLeastTwo] [n.AtLeastTwo] :
-    (ofNat m : R) = ofNat n ↔ (ofNat m : ℕ) = ofNat n :=
+    (no_index (ofNat m) : R) = no_index (ofNat n) ↔ (ofNat m : ℕ) = ofNat n :=
   Nat.cast_inj
 
 end OfNat

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -561,7 +561,7 @@ theorem abs_sub_convergents_le' {b : K}
   refine' (abs_sub_convergents_le not_terminated_at_n).trans _
   -- One can show that `0 < (GeneralizedContinuedFraction.of v).denominators n` but it's easier
   -- to consider the case `(GeneralizedContinuedFraction.of v).denominators n = 0`.
-  rcases zero_le_of_denom.eq_or_gt with
+  rcases (zero_le_of_denom (K := K)).eq_or_gt with
     ((hB : (GeneralizedContinuedFraction.of v).denominators n = 0) | hB)
   · simp only [hB, MulZeroClass.mul_zero, MulZeroClass.zero_mul, div_zero, le_refl]
   · apply one_div_le_one_div_of_le

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -541,16 +541,22 @@ theorem next_eq (f : Hom C₁ C₂) {i j : ι} (w : c.Rel i j) :
   simp only [xNextIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]
 #align homological_complex.hom.next_eq HomologicalComplex.Hom.next_eq
 
-@[reassoc (attr := simp 1100), elementwise (attr := simp)]
+@[reassoc, elementwise] -- @[simp] -- Porting note: simp can prove this
 theorem comm_from (f : Hom C₁ C₂) (i : ι) : f.f i ≫ C₂.dFrom i = C₁.dFrom i ≫ f.next i :=
   f.comm _ _
 #align homological_complex.hom.comm_from HomologicalComplex.Hom.comm_from
 
-@[reassoc (attr := simp 1100), elementwise (attr := simp)]
+attribute [simp 1100] comm_from_assoc
+attribute [simp] comm_from_apply
+
+@[reassoc, elementwise] -- @[simp] -- Porting note: simp can prove this
 theorem comm_to (f : Hom C₁ C₂) (j : ι) : f.prev j ≫ C₂.dTo j = C₁.dTo j ≫ f.f j :=
   f.comm _ _
 #align homological_complex.hom.comm_to HomologicalComplex.Hom.comm_to
 
+attribute [simp 1100] comm_to_assoc
+attribute [simp] comm_to_apply
+
 /-- A morphism of chain complexes
 induces a morphism of arrows of the differentials out of each object.
 -/
@@ -863,7 +869,6 @@ theorem mkHom_f_succ_succ (n : ℕ) :
             (mkHom P Q zero one one_zero_comm succ).f (n + 1),
             (mkHom P Q zero one one_zero_comm succ).comm (n + 1) n⟩).1 := by
   dsimp [mkHom, mkHomAux]
-  induction n <;> congr
 #align chain_complex.mk_hom_f_succ_succ ChainComplex.mkHom_f_succ_succ
 
 end MkHom
@@ -1113,7 +1118,6 @@ theorem mkHom_f_succ_succ (n : ℕ) :
             (mkHom P Q zero one one_zero_comm succ).f (n + 1),
             (mkHom P Q zero one one_zero_comm succ).comm n (n + 1)⟩).1 := by
   dsimp [mkHom, mkHomAux]
-  induction n <;> congr
 #align cochain_complex.mk_hom_f_succ_succ CochainComplex.mkHom_f_succ_succ
 
 end MkHom

Mathlib/Algebra/Homology/Homology.lean

@@ -205,11 +205,14 @@ abbrev cyclesMap (f : C₁ ⟶ C₂) (i : ι) : (C₁.cycles i : V) ⟶ (C₂.cy
 #align cycles_map cyclesMap
 
 -- Porting note: Originally `@[simp, reassoc.1, elementwise]`
-@[reassoc (attr := simp 1100), elementwise (attr := simp)]
+@[reassoc, elementwise] -- @[simp] -- Porting note: simp can prove this
 theorem cyclesMap_arrow (f : C₁ ⟶ C₂) (i : ι) :
     cyclesMap f i ≫ (C₂.cycles i).arrow = (C₁.cycles i).arrow ≫ f.f i := by simp
 #align cycles_map_arrow cyclesMap_arrow
 
+attribute [simp 1100] cyclesMap_arrow_assoc
+attribute [simp] cyclesMap_arrow_apply
+
 @[simp]
 theorem cyclesMap_id (i : ι) : cyclesMap (𝟙 C₁) i = 𝟙 _ := by
   dsimp only [cyclesMap]