chore: move to v4.6.0-rc1, merging adaptations from bump/v4.6.0 (#10176)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

.github/workflows/bors.yml

@@ -284,7 +284,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.5.0-rc1
+          git checkout toolchain/v4.6.0-rc1
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

.github/workflows/build.yml

@@ -291,7 +291,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.5.0-rc1
+          git checkout toolchain/v4.6.0-rc1
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

.github/workflows/build.yml.in

@@ -270,7 +270,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.5.0-rc1
+          git checkout toolchain/v4.6.0-rc1
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

.github/workflows/build_fork.yml

@@ -288,7 +288,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.5.0-rc1
+          git checkout toolchain/v4.6.0-rc1
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

Archive/Examples/IfNormalization/Result.lean

@@ -99,7 +99,7 @@ def normalize (l : AList (fun _ : ℕ => Bool)) :
           by_cases w = v <;> ◾⟩
     | some b =>
       have i' := normalize l (.ite (lit b) t e); ⟨i'.1, ◾⟩
-  termination_by normalize e => e.normSize
+  termination_by e => e.normSize
 
 /-
 We recall the statement of the if-normalization problem.

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -116,7 +116,7 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
     | some b =>
       have ⟨e', he'⟩ := normalize' l (.ite (lit b) t e)
       ⟨e', by simp_all⟩
-  termination_by normalize' e => e.normSize'
+  termination_by e' => e'.normSize'
 
 example : IfNormalization :=
   ⟨fun e => (normalize' ∅ e).1,

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -171,7 +171,7 @@ theorem countedSequence_finite : ∀ p q : ℕ, (countedSequence p q).Finite
     rw [counted_succ_succ, Set.finite_union, Set.finite_image_iff (List.cons_injective.injOn _),
       Set.finite_image_iff (List.cons_injective.injOn _)]
     exact ⟨countedSequence_finite _ _, countedSequence_finite _ _⟩
-termination_by _ p q => p + q -- Porting note: Added `termination_by`
+termination_by p q => p + q -- Porting note: Added `termination_by`
 #align ballot.counted_sequence_finite Ballot.countedSequence_finite
 
 theorem countedSequence_nonempty : ∀ p q : ℕ, (countedSequence p q).Nonempty
@@ -215,7 +215,7 @@ theorem count_countedSequence : ∀ p q : ℕ, count (countedSequence p q) = (p
       count_injective_image List.cons_injective, count_countedSequence _ _]
     · norm_cast
       rw [add_assoc, add_comm 1 q, ← Nat.choose_succ_succ, Nat.succ_eq_add_one, add_right_comm]
-termination_by _ p q => p + q -- Porting note: Added `termination_by`
+termination_by p q => p + q -- Porting note: Added `termination_by`
 #align ballot.count_counted_sequence Ballot.count_countedSequence
 
 theorem first_vote_pos :

Counterexamples/CharPZeroNeCharZero.lean

@@ -34,7 +34,7 @@ theorem withZero_unit_charP_zero : CharP (WithZero Unit) 0 :=
 #align counterexample.with_zero_unit_char_p_zero Counterexample.withZero_unit_charP_zero
 
 theorem withZero_unit_not_charZero : ¬CharZero (WithZero Unit) := fun ⟨h⟩ =>
-  h.ne (by simp : 1 + 1 ≠ 0 + 1) (by simp)
+  h.ne (by simp : 1 + 1 ≠ 0 + 1) (by set_option simprocs false in simp)
 #align counterexample.with_zero_unit_not_char_zero Counterexample.withZero_unit_not_charZero
 
 end Counterexample

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -491,7 +491,7 @@ end CategoryTheory.Aut
 instance GroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget GroupCat.{u}) where
   reflects {X Y} f _ := by
     let i := asIso ((forget GroupCat).map f)
-    let e : X ≃* Y := { i.toEquiv with map_mul' := by aesop }
+    let e : X ≃* Y := { i.toEquiv with map_mul' := map_mul _ }
     exact IsIso.of_iso e.toGroupCatIso
 set_option linter.uppercaseLean3 false in
 #align Group.forget_reflects_isos GroupCat.forget_reflects_isos
@@ -502,7 +502,7 @@ set_option linter.uppercaseLean3 false in
 instance CommGroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommGroupCat.{u}) where
   reflects {X Y} f _ := by
     let i := asIso ((forget CommGroupCat).map f)
-    let e : X ≃* Y := { i.toEquiv with map_mul' := by aesop }
+    let e : X ≃* Y := { i.toEquiv with map_mul' := map_mul _}
     exact IsIso.of_iso e.toCommGroupCatIso
 set_option linter.uppercaseLean3 false in
 #align CommGroup.forget_reflects_isos CommGroupCat.forget_reflects_isos

Mathlib/Algebra/DirectLimit.lean

@@ -719,7 +719,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
         have := DirectedSystem.map_map (fun i j h => f' i j h) hij (le_refl j : j ≤ j)
         rw [this]
         exact sub_self _
-        exacts [Or.inr rfl, Or.inl rfl]
+        exacts [Or.inl rfl, Or.inr rfl]
     · refine' ⟨i, {⟨i, 1⟩}, _, isSupported_sub (isSupported_of.2 rfl) isSupported_one, _⟩
       · rintro k (rfl | h)
         rfl

Mathlib/Algebra/DirectSum/Basic.lean

@@ -309,7 +309,7 @@ variable {α : Option ι → Type w} [∀ i, AddCommMonoid (α i)]
 -- include dec_ι
 
 /-- Isomorphism obtained by separating the term of index `none` of a direct sum over `Option ι`.-/
-@[simps]
+@[simps!]
 noncomputable def addEquivProdDirectSum : (⨁ i, α i) ≃+ α none × ⨁ i, α (some i) :=
   { DFinsupp.equivProdDFinsupp with map_add' := DFinsupp.equivProdDFinsupp_add }
 #align direct_sum.add_equiv_prod_direct_sum DirectSum.addEquivProdDirectSum

Mathlib/Algebra/EuclideanDomain/Defs.lean

@@ -186,7 +186,7 @@ theorem GCD.induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x)
   else
     have _ := mod_lt b a0
     H1 _ _ a0 (GCD.induction (b % a) a H0 H1)
-termination_by _ => a
+termination_by a
 #align euclidean_domain.gcd.induction EuclideanDomain.GCD.induction
 
 end
@@ -202,7 +202,7 @@ def gcd (a b : R) : R :=
   else
     have _ := mod_lt b a0
     gcd (b % a) a
-termination_by _ => a
+termination_by a
 #align euclidean_domain.gcd EuclideanDomain.gcd
 
 @[simp]
@@ -226,7 +226,7 @@ def xgcdAux (r s t r' s' t' : R) : R × R × R :=
     let q := r' / r
     have _ := mod_lt r' _hr
     xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
-termination_by _ => r
+termination_by r
 #align euclidean_domain.xgcd_aux EuclideanDomain.xgcdAux
 
 @[simp]

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -355,11 +355,11 @@ theorem gcd_assoc' [GCDMonoid α] (m n k : α) : Associated (gcd (gcd m n) k) (g
       ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_right n k)))
 #align gcd_assoc' gcd_assoc'
 
-instance [NormalizedGCDMonoid α] : IsCommutative α gcd :=
-  ⟨gcd_comm⟩
+instance [NormalizedGCDMonoid α] : Std.Commutative (α := α) gcd where
+  comm := gcd_comm
 
-instance [NormalizedGCDMonoid α] : IsAssociative α gcd :=
-  ⟨gcd_assoc⟩
+instance [NormalizedGCDMonoid α] : Std.Associative (α := α) gcd where
+  assoc := gcd_assoc
 
 theorem gcd_eq_normalize [NormalizedGCDMonoid α] {a b c : α} (habc : gcd a b ∣ c)
     (hcab : c ∣ gcd a b) : gcd a b = normalize c :=
@@ -779,11 +779,11 @@ theorem lcm_assoc' [GCDMonoid α] (m n k : α) : Associated (lcm (lcm m n) k) (l
       (lcm_dvd ((dvd_lcm_right _ _).trans (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))
 #align lcm_assoc' lcm_assoc'
 
-instance [NormalizedGCDMonoid α] : IsCommutative α lcm :=
-  ⟨lcm_comm⟩
+instance [NormalizedGCDMonoid α] : Std.Commutative (α := α) lcm where
+  comm := lcm_comm
 
-instance [NormalizedGCDMonoid α] : IsAssociative α lcm :=
-  ⟨lcm_assoc⟩
+instance [NormalizedGCDMonoid α] : Std.Associative (α := α) lcm where
+  assoc := lcm_assoc
 
 theorem lcm_eq_normalize [NormalizedGCDMonoid α] {a b c : α} (habc : lcm a b ∣ c)
     (hcab : c ∣ lcm a b) : lcm a b = normalize c :=

Mathlib/Algebra/Group/Basic.lean

@@ -76,7 +76,7 @@ section Semigroup
 variable [Semigroup α]
 
 @[to_additive]
-instance Semigroup.to_isAssociative : IsAssociative α (· * ·) := ⟨mul_assoc⟩
+instance Semigroup.to_isAssociative : Std.Associative (α := α)  (· * ·) := ⟨mul_assoc⟩
 #align semigroup.to_is_associative Semigroup.to_isAssociative
 #align add_semigroup.to_is_associative AddSemigroup.to_isAssociative
 
@@ -105,7 +105,7 @@ theorem comp_mul_right (x y : α) : (· * x) ∘ (· * y) = (· * (y * x)) := by
 end Semigroup
 
 @[to_additive]
-instance CommMagma.to_isCommutative [CommMagma G] : IsCommutative G (· * ·) := ⟨mul_comm⟩
+instance CommMagma.to_isCommutative [CommMagma G] : Std.Commutative (α := G) (· * ·) := ⟨mul_comm⟩
 #align comm_semigroup.to_is_commutative CommMagma.to_isCommutative
 #align add_comm_semigroup.to_is_commutative AddCommMagma.to_isCommutative
 

Mathlib/Algebra/Group/Equiv/TypeTags.lean

@@ -109,14 +109,14 @@ abbrev MulEquiv.toAdditive'' [AddZeroClass G] [MulOneClass H] :
 
 /-- Multiplicative equivalence between multiplicative endomorphisms of a `MulOneClass` `M`
 and additive endomorphisms of `Additive M`. -/
-@[simps] def monoidEndToAdditive (M : Type*) [MulOneClass M] :
+@[simps!] def monoidEndToAdditive (M : Type*) [MulOneClass M] :
     Monoid.End M ≃* AddMonoid.End (Additive M) :=
   { MonoidHom.toAdditive with
     map_mul' := fun _ _ => rfl }
 
 /-- Multiplicative equivalence between additive endomorphisms of an `AddZeroClass` `A`
 and multiplicative endomorphisms of `Multiplicative A`. -/
-@[simps] def addMonoidEndToMultiplicative (A : Type*) [AddZeroClass A] :
+@[simps!] def addMonoidEndToMultiplicative (A : Type*) [AddZeroClass A] :
     AddMonoid.End A ≃* Monoid.End (Multiplicative A) :=
   { AddMonoidHom.toMultiplicative with
     map_mul' := fun _ _ => rfl }

Mathlib/Algebra/Group/WithOne/Defs.lean

@@ -184,8 +184,8 @@ attribute [elab_as_elim] WithZero.cases_on
 instance mulOneClass [Mul α] : MulOneClass (WithOne α) where
   mul := (· * ·)
   one := 1
-  one_mul := (Option.liftOrGet_isLeftId _).1
-  mul_one := (Option.liftOrGet_isRightId _).1
+  one_mul := (Option.liftOrGet_isId _).left_id
+  mul_one := (Option.liftOrGet_isId _).right_id
 
 @[to_additive (attr := simp, norm_cast)]
 lemma coe_mul [Mul α] (a b : α) : (↑(a * b) : WithOne α) = a * b := rfl

Mathlib/Algebra/Lie/Abelian.lean

@@ -89,8 +89,9 @@ theorem lie_abelian_iff_equiv_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : T
 #align lie_abelian_iff_equiv_lie_abelian lie_abelian_iff_equiv_lie_abelian
 
 theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [Ring A] :
-    IsCommutative A (· * ·) ↔ IsLieAbelian A := by
-  have h₁ : IsCommutative A (· * ·) ↔ ∀ a b : A, a * b = b * a := ⟨fun h => h.1, fun h => ⟨h⟩⟩
+    Std.Commutative (α := A) (· * ·) ↔ IsLieAbelian A := by
+  have h₁ : Std.Commutative (α := A) (· * ·) ↔ ∀ a b : A, a * b = b * a :=
+    ⟨fun h => h.1, fun h => ⟨h⟩⟩
   have h₂ : IsLieAbelian A ↔ ∀ a b : A, ⁅a, b⁆ = 0 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
   simp only [h₁, h₂, LieRing.of_associative_ring_bracket, sub_eq_zero]
 #align commutative_ring_iff_abelian_lie_ring commutative_ring_iff_abelian_lie_ring

Mathlib/Algebra/Lie/DirectSum.lean

@@ -170,7 +170,7 @@ def lieAlgebraOf [DecidableEq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i :=
         -- with `simp [of, singleAddHom]`
         simp only [of, singleAddHom, bracket_apply]
         erw [AddHom.coe_mk, single_apply, single_apply]
-        simp? [h] says simp only [h, dite_eq_ite, ite_true, single_apply]
+        simp? [h] says simp only [h, ↓reduceDite, single_apply]
         intros
         erw [single_add]
       · -- This used to be the end of the proof before leanprover/lean4#2644

Mathlib/Algebra/Lie/Subalgebra.lean

@@ -193,7 +193,6 @@ theorem mk_coe (S : Set L) (h₁ h₂ h₃ h₄) :
   rfl
 #align lie_subalgebra.mk_coe LieSubalgebra.mk_coe
 
-@[simp]
 theorem coe_to_submodule_mk (p : Submodule R L) (h) :
     (({ p with lie_mem' := h } : LieSubalgebra R L) : Submodule R L) = p := by
   cases p

Mathlib/Algebra/Lie/Submodule.lean

@@ -128,7 +128,6 @@ theorem coe_toSet_mk (S : Set M) (h₁ h₂ h₃ h₄) :
   rfl
 #align lie_submodule.coe_to_set_mk LieSubmodule.coe_toSet_mk
 
-@[simp]
 theorem coe_toSubmodule_mk (p : Submodule R M) (h) :
     (({ p with lie_mem := h } : LieSubmodule R L M) : Submodule R M) = p := by cases p; rfl
 #align lie_submodule.coe_to_submodule_mk LieSubmodule.coe_toSubmodule_mk

Mathlib/Algebra/Lie/Weights/Linear.lean

@@ -76,13 +76,13 @@ instance instLinearWeightsOfIsLieAbelian [IsLieAbelian L] [NoZeroSMulDivisors R
       rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero]
     intro χ hχ x y
     simp_rw [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, weightSpace, weightSpaceOf,
-      LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule, Submodule.eta] at hχ
+      LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule] at hχ
     exact Module.End.map_add_of_iInf_generalizedEigenspace_ne_bot_of_commute
       (toEndomorphism R L M).toLinearMap χ hχ h x y
   { map_add := aux
     map_smul := fun χ hχ t x ↦ by
       simp_rw [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, weightSpace, weightSpaceOf,
-        LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule, Submodule.eta] at hχ
+        LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule] at hχ
       exact Module.End.map_smul_of_iInf_generalizedEigenspace_ne_bot
         (toEndomorphism R L M).toLinearMap χ hχ t x
     map_lie := fun χ hχ t x ↦ by

Mathlib/Algebra/Module/Injective.lean

@@ -184,10 +184,6 @@ def ExtensionOf.max {c : Set (ExtensionOf i f)} (hchain : IsChain (· ≤ ·) c)
       refine' le_trans hnonempty.some.le <|
         (LinearPMap.le_sSup _ <|
             (Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩).1
-      -- porting note: this subgoal didn't exist before the reenableeta branch
-      -- follow-up note: the subgoal was moved from after `refine'` in `is_extension` to here
-      -- after the behavior of `refine'` changed.
-      exact (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain)
     is_extension := fun m => by
       refine' Eq.trans (hnonempty.some.is_extension m) _
       symm

Mathlib/Algebra/Order/WithZero.lean

@@ -285,4 +285,4 @@ instance : LinearOrderedAddCommGroupWithTop (Additive αᵒᵈ) :=
   { Additive.subNegMonoid, instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual,
     Additive.instNontrivial with
     neg_top := @inv_zero _ (_)
-    add_neg_cancel := fun a ha ↦ mul_inv_cancel (id ha : Additive.toMul a ≠ 0) }
+    add_neg_cancel := fun a ha ↦ mul_inv_cancel (G₀ := α) (id ha : Additive.toMul a ≠ 0) }

Mathlib/Algebra/Ring/BooleanRing.lean

@@ -54,7 +54,7 @@ section BooleanRing
 
 variable [BooleanRing α] (a b : α)
 
-instance : IsIdempotent α (· * ·) :=
+instance : Std.IdempotentOp (α := α) (· * ·) :=
   ⟨BooleanRing.mul_self⟩
 
 @[simp]

Mathlib/Algebra/Ring/Idempotents.lean

@@ -42,8 +42,8 @@ def IsIdempotentElem (p : M) : Prop :=
 
 namespace IsIdempotentElem
 
-theorem of_isIdempotent [IsIdempotent M (· * ·)] (a : M) : IsIdempotentElem a :=
-  IsIdempotent.idempotent a
+theorem of_isIdempotent [Std.IdempotentOp (α := M) (· * ·)] (a : M) : IsIdempotentElem a :=
+  Std.IdempotentOp.idempotent a
 #align is_idempotent_elem.of_is_idempotent IsIdempotentElem.of_isIdempotent
 
 theorem eq {p : M} (h : IsIdempotentElem p) : p * p = p :=

Mathlib/Algebra/Ring/Pi.lean

@@ -134,7 +134,7 @@ variable {I : Type u}
 
 /-- Evaluation of functions into an indexed collection of non-unital rings at a point is a
 non-unital ring homomorphism. This is `Function.eval` as a `NonUnitalRingHom`. -/
-@[simps]
+@[simps!]
 def Pi.evalNonUnitalRingHom (f : I → Type v) [∀ i, NonUnitalNonAssocSemiring (f i)] (i : I) :
     (∀ i, f i) →ₙ+* f i :=
   { Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }

Mathlib/Analysis/Analytic/Composition.lean

@@ -1165,9 +1165,9 @@ def sigmaEquivSigmaPi (n : ℕ) :
       rw [get_of_eq (splitWrtComposition_join _ _ _)]
       · simp only [get_ofFn]
         rfl
-      · congr
       · simp only [map_ofFn]
         rfl
+      · congr
 #align composition.sigma_equiv_sigma_pi Composition.sigmaEquivSigmaPi
 
 end Composition

Mathlib/Analysis/Fourier/AddCircle.lean

@@ -358,7 +358,8 @@ theorem fourierCoeff_eq_intervalIntegral (f : AddCircle T → E) (n : ℤ) (a :
     fourierCoeff f n = (1 / T) • ∫ x in a..a + T, @fourier T (-n) x • f x := by
   have : ∀ x : ℝ, @fourier T (-n) x • f x = (fun z : AddCircle T => @fourier T (-n) z • f z) x := by
     intro x; rfl
-  simp_rw [this]
+  -- After leanprover/lean4#3124, we need to add `singlePass := true` to avoid an infinite loop.
+  simp_rw (config := {singlePass := true}) [this]
   rw [fourierCoeff, AddCircle.intervalIntegral_preimage T a (fun z => _ • _),
     volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
     ← smul_assoc, smul_eq_mul, one_div_mul_cancel hT.out.ne', one_smul]

Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

@@ -53,7 +53,7 @@ local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y
 and outputs a set of orthogonal vectors which have the same span. -/
 noncomputable def gramSchmidt [IsWellOrder ι (· < ·)] (f : ι → E) (n : ι) : E :=
   f n - ∑ i : Iio n, orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
-termination_by _ n => n
+termination_by n
 decreasing_by exact mem_Iio.1 i.2
 #align gram_schmidt gramSchmidt
 
@@ -152,7 +152,7 @@ theorem gramSchmidt_mem_span (f : ι → E) :
   let hkj : k < j := (Finset.mem_Iio.1 hk).trans_le hij
   exact smul_mem _ _
     (span_mono (image_subset f <| Iic_subset_Iic.2 hkj.le) <| gramSchmidt_mem_span _ le_rfl)
-termination_by _ => j
+termination_by j => j
 decreasing_by exact hkj
 #align gram_schmidt_mem_span gramSchmidt_mem_span
 

Mathlib/Analysis/NormedSpace/AffineIsometry.lean

@@ -876,7 +876,7 @@ namespace AffineSubspace
 /-- An affine subspace is isomorphic to its image under an injective affine map.
 This is the affine version of `Submodule.equivMapOfInjective`.
 -/
-@[simps]
+@[simps linear, simps! toFun]
 noncomputable def equivMapOfInjective (E : AffineSubspace 𝕜 P₁) [Nonempty E] (φ : P₁ →ᵃ[𝕜] P₂)
     (hφ : Function.Injective φ) : E ≃ᵃ[𝕜] E.map φ :=
   { Equiv.Set.image _ (E : Set P₁) hφ with

Mathlib/CategoryTheory/Monad/EquivMon.lean

@@ -98,8 +98,8 @@ def monToMonad : Mon_ (C ⥤ C) ⥤ Monad C where
         intro Z
         erw [← NatTrans.comp_app, f.mul_hom]
         dsimp
-        simp only [NatTrans.naturality, NatTrans.hcomp_app, assoc, NatTrans.comp_app,
-          ofMon_μ] }
+        simp only [Category.assoc, NatTrans.naturality, ofMon_obj]
+        rfl }
 #align category_theory.Monad.Mon_to_Monad CategoryTheory.Monad.monToMonad
 
 /-- Oh, monads are just monoids in the category of endofunctors (equivalence of categories). -/

Mathlib/CategoryTheory/Monoidal/Mod_.lean

@@ -114,6 +114,7 @@ set_option linter.uppercaseLean3 false in
 
 open CategoryTheory.MonoidalCategory
 
+set_option maxHeartbeats 400000 in
 /-- A morphism of monoid objects induces a "restriction" or "comap" functor
 between the categories of module objects.
 -/