diff --git a/Mathlib/Algebra/Algebra/Defs.lean b/Mathlib/Algebra/Algebra/Defs.lean
index 3baf9f1f0a2552..d847d42b94ed89 100644
--- a/Mathlib/Algebra/Algebra/Defs.lean
+++ b/Mathlib/Algebra/Algebra/Defs.lean
@@ -382,11 +382,8 @@ theorem coe_linearMap : ⇑(Algebra.linearMap R A) = algebraMap R A :=
 
 /-- The identity map inducing an `Algebra` structure. -/
 instance (priority := 1100) 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].
   toSMul := instSMulOfMul
-  __ := ({ RingHom.id R with toFun x := x }).toAlgebra
+  __ := (RingHom.id R).toAlgebra
 
 @[simp] lemma linearMap_self : Algebra.linearMap R R = .id := rfl
 
diff --git a/Mathlib/Algebra/Ring/Hom/Defs.lean b/Mathlib/Algebra/Ring/Hom/Defs.lean
index a3f0f3bdb9d5ad..d636309455dc5f 100644
--- a/Mathlib/Algebra/Ring/Hom/Defs.lean
+++ b/Mathlib/Algebra/Ring/Hom/Defs.lean
@@ -506,6 +506,7 @@ def mk' [NonAssocSemiring α] [NonAssocRing β] (f : α →* β)
 variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β}
 
 /-- The identity ring homomorphism from a semiring to itself. -/
+@[implicit_reducible]
 def id (α : Type*) [NonAssocSemiring α] : α →+* α where
   toFun := _root_.id
   map_zero' := rfl