chore (Algebra.Basic): make RingHom.id and related declarations reducible

Mathlib/Algebra/Algebra/Basic.lean

@@ -247,7 +247,7 @@ end FieldDivisionRing
 end algebraMap
 
 /-- Creating an algebra from a morphism to the center of a semiring. -/
-def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
+@[reducible] def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
     (h : ∀ c x, i c * x = x * i c) : Algebra R S where
   smul c x := i c * x
   commutes' := h
@@ -256,7 +256,8 @@ def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
 #align ring_hom.to_algebra' RingHom.toAlgebra'
 
 /-- Creating an algebra from a morphism to a commutative semiring. -/
-def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
+@[reducible] def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) :
+    Algebra R S :=
   i.toAlgebra' fun _ => mul_comm _
 #align ring_hom.to_algebra RingHom.toAlgebra
 
@@ -431,7 +432,7 @@ theorem coe_linearMap : ⇑(Algebra.linearMap R A) = algebraMap R A :=
   rfl
 #align algebra.coe_linear_map Algebra.coe_linearMap
 
-instance id : Algebra R R :=
+@[reducible] instance id : Algebra R R :=
   (RingHom.id R).toAlgebra
 #align algebra.id Algebra.id
 

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -997,7 +997,7 @@ def MulHom.id (M : Type*) [Mul M] : M →ₙ* M where
 #align mul_hom.id_apply MulHom.id_apply
 
 /-- The identity map from a monoid to itself. -/
-@[to_additive (attr := simps)]
+@[to_additive (attr := simps, reducible)]
 def MonoidHom.id (M : Type*) [MulOneClass M] : M →* M where
   toFun x := x
   map_one' := rfl

Mathlib/Algebra/Lie/BaseChange.lean

@@ -60,6 +60,7 @@ private theorem bracket_def (x : A ⊗[R] L) (m : A ⊗[R] M) : ⁅x, m⁆ = bra
 theorem bracket_tmul (s t : A) (x : L) (y : M) : ⁅s ⊗ₜ[R] x, t ⊗ₜ[R] y⁆ = (s * t) ⊗ₜ ⁅x, y⁆ := rfl
 #align lie_algebra.extend_scalars.bracket_tmul LieAlgebra.ExtendScalars.bracket_tmul
 
+set_option maxHeartbeats 12800000 in
 private theorem bracket_lie_self (x : A ⊗[R] L) : ⁅x, x⁆ = 0 := by
   simp only [bracket_def]
   refine' x.induction_on _ _ _

Mathlib/Algebra/Lie/Killing.lean

@@ -207,6 +207,7 @@ lemma eq_zero_of_mem_weightSpace_mem_posFitting [LieAlgebra.IsNilpotent R L]
   obtain ⟨m, rfl⟩ := (mem_posFittingCompOf R x m₁).mp hm₁ k
   simp [hB, hk]
 
+set_option maxHeartbeats 1600000 in
 lemma trace_toEndomorphism_eq_zero_of_mem_lcs
     {k : ℕ} {x : L} (hk : 1 ≤ k) (hx : x ∈ lowerCentralSeries R L L k) :
     trace R _ (toEndomorphism R L M x) = 0 := by

Mathlib/Algebra/Lie/Submodule.lean

@@ -823,7 +823,7 @@ def map : LieSubmodule R L M' :=
     lie_mem := fun {x m'} h ↦ by
       rcases h with ⟨m, hm, hfm⟩; use ⁅x, m⁆; constructor
       · apply N.lie_mem hm
-      · norm_cast at hfm; simp [hfm] }
+      · norm_cast at hfm; simp only [LieModuleHom.coe_toLinearMap, LieModuleHom.map_lie]; erw [hfm]}
 #align lie_submodule.map LieSubmodule.map
 
 @[simp] theorem coe_map : (N.map f : Set M') = f '' N := rfl

Mathlib/Algebra/Ring/Equiv.lean

@@ -746,7 +746,6 @@ theorem toRingHom_refl : (RingEquiv.refl R).toRingHom = RingHom.id R :=
   rfl
 #align ring_equiv.to_ring_hom_refl RingEquiv.toRingHom_refl
 
-@[simp]
 theorem toMonoidHom_refl : (RingEquiv.refl R).toMonoidHom = MonoidHom.id R :=
   rfl
 #align ring_equiv.to_monoid_hom_refl RingEquiv.toMonoidHom_refl

Mathlib/Algebra/Ring/Hom/Defs.lean

@@ -629,8 +629,8 @@ def mk' [NonAssocSemiring α] [NonAssocRing β] (f : α →* β)
 variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β}
 
 /-- The identity ring homomorphism from a semiring to itself. -/
-def id (α : Type*) [NonAssocSemiring α] : α →+* α := by
-  refine' { toFun := _root_.id.. } <;> intros <;> rfl
+@[reducible] def id (α : Type*) [NonAssocSemiring α] : α →+* α :=
+  { AddMonoidHom.id α, MonoidHom.id α with }
 #align ring_hom.id RingHom.id
 
 instance : Inhabited (α →+* α) :=
@@ -646,7 +646,6 @@ theorem coe_addMonoidHom_id : (id α : α →+ α) = AddMonoidHom.id α :=
   rfl
 #align ring_hom.coe_add_monoid_hom_id RingHom.coe_addMonoidHom_id
 
-@[simp]
 theorem coe_monoidHom_id : (id α : α →* α) = MonoidHom.id α :=
   rfl
 #align ring_hom.coe_monoid_hom_id RingHom.coe_monoidHom_id

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -404,6 +404,7 @@ theorem mem_carrier_iff' (q : Spec.T A⁰_ f) (a : A) :
         dsimp only [Subtype.coe_mk]; rw [← hx]; rfl)
 #align algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.mem_carrier_iff' AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff'
 
+set_option maxHeartbeats 400000 in
 theorem carrier.add_mem (q : Spec.T A⁰_ f) {a b : A} (ha : a ∈ carrier f_deg q)
     (hb : b ∈ carrier f_deg q) : a + b ∈ carrier f_deg q := by
   refine' fun i => (q.2.mem_or_mem _).elim id id

Mathlib/Analysis/Calculus/LagrangeMultipliers.lean

@@ -121,6 +121,7 @@ theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt {ι : Type*} [Fint
   · ext x; simpa [mul_comm] using hsum x
 #align is_local_extr_on.exists_multipliers_of_has_strict_fderiv_at IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt
 
+set_option maxHeartbeats 400000 in
 /-- Lagrange multipliers theorem. Let `f : ι → E → ℝ` be a finite family of functions.
 Suppose that `φ : E → ℝ` has a local extremum on the set `{x | ∀ i, f i x = f i x₀}` at `x₀`.
 Suppose that all functions `f i` as well as `φ` are strictly differentiable at `x₀`.

Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean

@@ -106,7 +106,6 @@ theorem WeakDual.CharacterSpace.mem_spectrum_iff_exists {a : A} {z : ℂ} :
     simp only [map_sub, sub_eq_zero, AlgHomClass.commutes, Algebra.id.map_eq_id,
       RingHom.id_apply] at hf
     refine ⟨f, ?_⟩
-    rw [AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply] at hf
     exact hf.symm
   · rintro ⟨f, rfl⟩
     exact AlgHom.apply_mem_spectrum f a

Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

@@ -91,6 +91,7 @@ def polarCoord : PartialHomeomorph (ℝ × ℝ) (ℝ × ℝ) where
     · exact Complex.equivRealProdClm.symm.continuous.continuousOn
 #align polar_coord polarCoord
 
+set_option maxHeartbeats 800000 in
 theorem hasFDerivAt_polarCoord_symm (p : ℝ × ℝ) :
     HasFDerivAt polarCoord.symm
       (LinearMap.toContinuousLinearMap (Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)

Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean

@@ -28,6 +28,7 @@ open Filter
 
 namespace Complex
 
+set_option maxHeartbeats 1600000 in
 theorem hasStrictFDerivAt_cpow {p : ℂ × ℂ} (hp : 0 < p.1.re ∨ p.1.im ≠ 0) :
     HasStrictFDerivAt (fun x : ℂ × ℂ => x.1 ^ x.2)
       ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ +

Mathlib/Geometry/Manifold/Instances/Sphere.lean

@@ -142,6 +142,7 @@ theorem stereoInvFunAux_mem (hv : ‖v‖ = 1) {w : E} (hw : w ∈ (ℝ ∙ v)
   ring
 #align stereo_inv_fun_aux_mem stereoInvFunAux_mem
 
+set_option synthInstance.maxHeartbeats 50000 in
 theorem hasFDerivAt_stereoInvFunAux (v : E) :
     HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0 := by
   have h₀ : HasFDerivAt (fun w : E => ‖w‖ ^ 2) (0 : E →L[ℝ] ℝ) 0 := by

Mathlib/LinearAlgebra/Basis.lean

@@ -1394,6 +1394,7 @@ def Submodule.inductionOnRankAux (b : Basis ι R M) (P : Submodule R M → Sort*
 
 end Induction
 
+set_option maxHeartbeats 3200000 in
 /-- An element of a non-unital-non-associative algebra is in the center exactly when it commutes
 with the basis elements. -/
 lemma Basis.mem_center_iff {A}

Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

@@ -295,7 +295,7 @@ def toQuaternion : CliffordAlgebra (Q c₁ c₂) →ₐ[R] ℍ[R,c₁,c₂] :=
   CliffordAlgebra.lift (Q c₁ c₂)
     ⟨{  toFun := fun v => (⟨0, v.1, v.2, 0⟩ : ℍ[R,c₁,c₂])
         map_add' := fun v₁ v₂ => by simp
-        map_smul' := fun r v => by dsimp; rw [mul_zero]; rfl }, fun v => by
+        map_smul' := fun r v => by dsimp; rw [mul_zero] }, fun v => by
       dsimp
       ext
       all_goals dsimp; ring⟩

Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

@@ -216,6 +216,7 @@ theorem BilinForm.toMatrix'_apply (B : BilinForm R₂ (n → R₂)) (i j : n) :
   rfl
 #align bilin_form.to_matrix'_apply BilinForm.toMatrix'_apply
 
+set_option maxHeartbeats 1600000 in
 -- Porting note: dot notation for bundled maps doesn't work in the rest of this section
 @[simp]
 theorem BilinForm.toMatrix'_comp (B : BilinForm R₂ (n → R₂)) (l r : (o → R₂) →ₗ[R₂] n → R₂) :
@@ -358,6 +359,7 @@ variable (c : Basis o R₂ M₂')
 
 variable [DecidableEq o]
 
+set_option maxHeartbeats 1600000 in
 -- Cannot be a `simp` lemma because `b` must be inferred.
 theorem BilinForm.toMatrix_comp (B : BilinForm R₂ M₂) (l r : M₂' →ₗ[R₂] M₂) :
     BilinForm.toMatrix c (B.comp l r) =

Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

@@ -279,6 +279,7 @@ variable [Fintype n'] [Fintype m']
 
 variable [DecidableEq n'] [DecidableEq m']
 
+set_option maxHeartbeats 400000 in
 @[simp]
 theorem LinearMap.toMatrix₂'_compl₁₂ (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (l : (n' → R) →ₗ[R] n → R)
     (r : (m' → R) →ₗ[R] m → R) :
@@ -438,6 +439,7 @@ variable [Fintype n'] [Fintype m']
 
 variable [DecidableEq n'] [DecidableEq m']
 
+set_option maxHeartbeats 3200000 in
 -- Cannot be a `simp` lemma because `b₁` and `b₂` must be inferred.
 theorem LinearMap.toMatrix₂_compl₁₂ (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (l : M₁' →ₗ[R] M₁)
     (r : M₂' →ₗ[R] M₂) :

Mathlib/LinearAlgebra/Prod.lean

@@ -273,6 +273,7 @@ theorem coprod_map_prod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : Su
     exact Set.image_prod fun m m₂ => f m + g m₂
 #align linear_map.coprod_map_prod LinearMap.coprod_map_prod
 
+set_option maxHeartbeats 400000 in
 /-- Taking the product of two maps with the same codomain is equivalent to taking the product of
 their domains.
 

Mathlib/RepresentationTheory/Character.lean

@@ -44,6 +44,7 @@ def character (V : FdRep k G) (g : G) :=
   LinearMap.trace k V (V.ρ g)
 #align fdRep.character FdRep.character
 
+set_option maxHeartbeats 1600000 in
 theorem char_mul_comm (V : FdRep k G) (g : G) (h : G) : V.character (h * g) = V.character (g * h) :=
   by simp only [trace_mul_comm, character, map_mul]
 #align fdRep.char_mul_comm FdRep.char_mul_comm

Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

@@ -99,6 +99,7 @@ namespace inhomogeneousCochains
 
 open Rep groupCohomology
 
+set_option maxHeartbeats 400000 in
 /-- The differential in the complex of inhomogeneous cochains used to
 calculate group cohomology. -/
 @[simps]

Mathlib/RingTheory/Kaehler.lean

@@ -268,7 +268,7 @@ def Derivation.liftKaehlerDifferential (D : Derivation R S M) : Ω[S⁄R] →ₗ
     refine Submodule.smul_induction_on hx ?_ ?_
     · rintro x (hx : _ = _) y -
       dsimp
-      rw [show ↑(x • y) = x * ↑y by rfl, Derivation.tensorProductTo_mul, hx, y.prop, zero_smul,
+      rw [Derivation.tensorProductTo_mul, hx, y.prop, zero_smul,
         zero_smul, zero_add]
     · intro x y ex ey; rw [map_add, ex, ey, zero_add]
 #align derivation.lift_kaehler_differential Derivation.liftKaehlerDifferential

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -335,6 +335,7 @@ instance : Semiring (MvPowerSeries σ R) :=
 
 end Semiring
 
+set_option maxHeartbeats 300000 in
 instance [CommSemiring R] : CommSemiring (MvPowerSeries σ R) :=
   { show Semiring (MvPowerSeries σ R) by infer_instance with
     mul_comm := fun φ ψ =>