Concretise submonoid

Mathlib/Algebra/Algebra/Hom.lean

@@ -508,13 +508,10 @@ lemma algebraMapSubmonoid_map_eq (f : A →ₐ[R] B) :
   ext x
   constructor
   · rintro ⟨a, ⟨r, hr, rfl⟩, rfl⟩
-    simp only [AlgHom.commutes]
-    use r
+    exact ⟨r, hr, by simp⟩
   · rintro ⟨r, hr, rfl⟩
     simp only [Submonoid.mem_map]
-    use (algebraMap R A r)
-    simp only [AlgHom.commutes, and_true]
-    use r
+    exact ⟨(algebraMap R A r), ⟨r, hr, by simp⟩, by simp⟩
 
 lemma algebraMapSubmonoid_le_comap (f : A →ₐ[R] B) :
     algebraMapSubmonoid A M ≤ (algebraMapSubmonoid B M).comap f.toRingHom := by

Mathlib/Algebra/Algebra/Operations.lean

@@ -751,7 +751,8 @@ theorem span_singleton_eq_one_iff {x : A} : span R {x} = 1 ↔ ∃ r : Rˣ, x =
   mpr := by rintro ⟨r, rfl⟩; exact span_singleton_algebraMap_of_isUnit r.isUnit
 
 theorem mker_spanSingleton :
-    MonoidHom.mker (Submodule.spanSingleton R) = (IsUnit.submonoid R).map (algebraMap R A) := by
+    (Submodule.spanSingleton R).toMonoidHom.mker =
+      (IsUnit.submonoid R).map (algebraMap R A).toMonoidHom := by
   ext; simp_rw [Submonoid.mem_map, IsUnit.mem_submonoid_iff, IsUnit, existsAndEq, true_and, eq_comm]
   exact span_singleton_eq_one_iff
 

Mathlib/Algebra/Category/Ring/Constructions.lean

@@ -162,7 +162,8 @@ lemma isPushout_iff_isPushout {R S : Type u} [CommRing R] [CommRing S] [Algebra
 lemma isPushout_of_isLocalization {R S Rₘ Sₘ : Type u}
     [CommRing R] [CommRing Rₘ] [Algebra R Rₘ] [CommRing S] [CommRing Sₘ] [Algebra S Sₘ]
     (f : R →+* S) (fₘ : Rₘ →+* Sₘ) (H : fₘ.comp (algebraMap _ _) = (algebraMap _ _).comp f)
-    (M : Submonoid R) [IsLocalization M Rₘ] [IsLocalization (M.map f) Sₘ] :
+    (M : Submonoid R) [IsLocalization M Rₘ]
+    [IsLocalization (M.map (MonoidHomClass.toMonoidHom f)) Sₘ] :
     IsPushout (CommRingCat.ofHom f) (CommRingCat.ofHom (algebraMap R Rₘ))
       (CommRingCat.ofHom (algebraMap S Sₘ)) (CommRingCat.ofHom fₘ) := by
   algebraize [f, fₘ, fₘ.comp (algebraMap R Rₘ)]

Mathlib/Algebra/Group/Subgroup/Actions.lean

@@ -79,4 +79,4 @@ end Subgroup
 open MonoidHom in
 lemma MonoidWithZeroHom.comap_mker {M N P : Type*} [MulZeroOneClass M] [MulZeroOneClass N]
     [MulZeroOneClass P] (g : N →*₀ P) (f : M →*₀ N) :
-    Submonoid.comap f (mker g) = mker (g.comp f) := rfl
+    Submonoid.comap f g.toMonoidHom.mker = (g.comp f).toMonoidHom.mker := rfl

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -428,8 +428,7 @@ theorem log_pow_int_eq_self {x : ℤ} (h : 1 < x.natAbs) (m : ℕ) : log (pow x
   (powLogEquiv (Int.pow_right_injective h)).symm_apply_apply _
 
 @[simp]
-theorem map_powers {N : Type*} {F : Type*} [Monoid N] [FunLike F M N] [MonoidHomClass F M N]
-    (f : F) (m : M) :
+theorem map_powers {N : Type*} [Monoid N] (f : M →* N) (m : M) :
     (powers m).map f = powers (f m) := by
   simp only [powers_eq_closure, map_mclosure f, Set.image_singleton]
 
@@ -495,7 +494,7 @@ variable [AddMonoid A]
 open Set
 
 theorem closure_singleton_eq (x : A) :
-    closure ({x} : Set A) = AddMonoidHom.mrange (multiplesHom A x) :=
+    closure ({x} : Set A) = (multiplesHom A x).mrange :=
   closure_eq_of_le (Set.singleton_subset_iff.2 ⟨1, one_nsmul x⟩) fun _ ⟨_n, hn⟩ =>
     hn ▸ nsmul_mem (subset_closure <| Set.mem_singleton _) _
 
@@ -509,7 +508,7 @@ theorem closure_singleton_zero : closure ({0} : Set A) = ⊥ := by
 
 /-- The additive submonoid generated by an element. -/
 def multiples (x : A) : AddSubmonoid A :=
-  AddSubmonoid.copy (AddMonoidHom.mrange (multiplesHom A x)) (Set.range (fun i => i • x : ℕ → A)) <|
+  AddSubmonoid.copy (multiplesHom A x).mrange (Set.range (fun i => i • x : ℕ → A)) <|
     Set.ext fun n => exists_congr fun i => by simp
 
 attribute [to_additive existing] Submonoid.powers