fix

Author: YaelDillies

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -288,7 +288,7 @@ def mapDomainAlgHom (f : M →* N) : A[M] →ₐ[R] A[N] where
 
 @[to_additive (attr := simp)]
 lemma mapDomainAlgHom_id : mapDomainAlgHom R A (.id M) = .id R A[M] := by
-  ext; simp [MonoidHom.id, ← Function.id_def]
+  ext; simp [MonoidHom.id, mapDomain, ← Function.id_def]
 
 @[to_additive (attr := simp)]
 lemma mapDomainAlgHom_comp (f : M →* N) (g : N →* O) :