chore(Algebra.Basic): override toFun and smul in Algebra.id (#9949)

mattrobball · mattrobball · commit 0aa016e0aae6 · 2024-01-24T18:17:19.000Z
The current definition of `Algebra.id` is `(RingHom.id _).toAlgebra`. The problem with this is that `RingHom.id` is a `def` and is not reducible. Thus Lean will often refuse to unfold it causing unification to fail unecessarily in typeclass searches. This overrides the data fields from `RingHom.id`.
diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean
@@ -436,8 +436,14 @@ theorem coe_linearMap : ⇑(Algebra.linearMap R A) = algebraMap R A :=
   rfl
 #align algebra.coe_linear_map Algebra.coe_linearMap
 
-instance id : Algebra R R :=
-  (RingHom.id R).toAlgebra
+/- The identity map inducing an `Algebra` structure. -/
+instance id : Algebra R R where
+  -- We override `toFun` and `toSMul` because `RingHom.id` is not reducible and cannot
+  -- be made so without a significant performance hit.
+  -- see library note [reducible non-instances].
+  toFun x := x
+  toSMul := Mul.toSMul _
+  __ := (RingHom.id R).toAlgebra
 #align algebra.id Algebra.id
 
 variable {R A}
diff --git a/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean b/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean
@@ -115,11 +115,8 @@ theorem WeakDual.CharacterSpace.mem_spectrum_iff_exists {a : A} {z : ℂ} :
     z ∈ spectrum ℂ a ↔ ∃ f : characterSpace ℂ A, f a = z := by
   refine' ⟨fun hz => _, _⟩
   · obtain ⟨f, hf⟩ := WeakDual.CharacterSpace.exists_apply_eq_zero hz
-    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
+    simp only [map_sub, sub_eq_zero, AlgHomClass.commutes] at hf
+    exact ⟨_, hf.symm⟩
   · rintro ⟨f, rfl⟩
     exact AlgHom.apply_mem_spectrum f a
 #align weak_dual.character_space.mem_spectrum_iff_exists WeakDual.CharacterSpace.mem_spectrum_iff_exists
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/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⟩
diff --git a/Mathlib/RingTheory/Kaehler.lean b/Mathlib/RingTheory/Kaehler.lean
@@ -268,8 +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,
-        zero_smul, zero_add]
+      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
 
diff --git a/test/Simp.lean b/test/Simp.lean
@@ -0,0 +1,20 @@
+import Mathlib.Algebra.Algebra.Pi
+import Mathlib.Algebra.Algebra.Basic
+
+/-!
+Tests for the behavior of `simp`.
+--/
+
+/- Taken from [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/
+  topic/simp.20.5BX.5D.20fails.2C.20rw.20.5BX.5D.20works) -/
+-- Example 1: succeeds
+example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
+    (r • f) a = r • (f a) := by
+  simp only [Pi.smul_apply] -- succeeds
+
+-- Example 2: used to fail, now succeeds!
+example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
+    (r • f) a = r • (f a) := by
+  let _ : SMul R R := SMulZeroClass.toSMul
+  simp only [Pi.smul_apply]
+
