diff --git a/Mathlib/Algebra/Category/Grp/Kernels.lean b/Mathlib/Algebra/Category/Grp/Kernels.lean
index 8f367b2c6f460..577c21325b183 100644
--- a/Mathlib/Algebra/Category/Grp/Kernels.lean
+++ b/Mathlib/Algebra/Category/Grp/Kernels.lean
@@ -26,7 +26,7 @@ def kernelCone : KernelFork f :=
 /-- The kernel of a group homomorphism is a kernel in the categorical sense. -/
 def kernelIsLimit : IsLimit <| kernelCone f :=
   Fork.IsLimit.mk _
-    (fun s => (by exact Fork.ι s : _ →+ G).codRestrict _ fun c => f.mem_ker.mpr <|
+    (fun s => (by exact Fork.ι s : _ →+ G).codRestrict _ fun c => mem_ker.mpr <|
       by exact DFunLike.congr_fun s.condition c)
     (fun _ => by rfl)
     (fun _ _ h => ext fun x => Subtype.ext_iff_val.mpr <| by exact DFunLike.congr_fun h x)
diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean
index 9a542a9b6014d..0d13d5ae72a71 100644
--- a/Mathlib/Algebra/Group/Subgroup/Basic.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean
@@ -2134,8 +2134,8 @@ def ker (f : G →* M) : Subgroup G :=
         f x⁻¹ = f x * f x⁻¹ := by rw [hx, one_mul]
         _ = 1 := by rw [← map_mul, mul_inv_cancel, map_one] }
 
-@[to_additive]
-theorem mem_ker (f : G →* M) {x : G} : x ∈ f.ker ↔ f x = 1 :=
+@[to_additive (attr := simp)]
+theorem mem_ker {f : G →* M} {x : G} : x ∈ f.ker ↔ f x = 1 :=
   Iff.rfl
 
 @[to_additive]
@@ -2155,7 +2155,7 @@ theorem ker_toHomUnits {M} [Monoid M] (f : G →* M) : f.toHomUnits.ker = f.ker
 theorem eq_iff (f : G →* M) {x y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker := by
   constructor <;> intro h
   · rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
-  · rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, f.mem_ker.1 h, mul_one]
+  · rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, mem_ker.1 h, mul_one]
 
 @[to_additive]
 instance decidableMemKer [DecidableEq M] (f : G →* M) : DecidablePred (· ∈ f.ker) := fun x =>
@@ -2226,7 +2226,7 @@ theorem range_le_ker_iff (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker 
 @[to_additive]
 instance (priority := 100) normal_ker (f : G →* M) : f.ker.Normal :=
   ⟨fun x hx y => by
-    rw [mem_ker, map_mul, map_mul, f.mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]⟩
+    rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]⟩
 
 @[to_additive (attr := simp)]
 lemma ker_fst : ker (fst G G') = .prod ⊥ ⊤ := SetLike.ext fun _ => (iff_of_eq (and_true _)).symm
@@ -2599,7 +2599,7 @@ See `MonoidHom.eq_liftOfRightInverse` for the uniqueness lemma.
 def liftOfRightInverse (hf : Function.RightInverse f_inv f) :
     { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃) where
   toFun g := f.liftOfRightInverseAux f_inv hf g.1 g.2
-  invFun φ := ⟨φ.comp f, fun x hx => (mem_ker _).mpr <| by simp [(mem_ker _).mp hx]⟩
+  invFun φ := ⟨φ.comp f, fun x hx ↦ mem_ker.mpr <| by simp [mem_ker.mp hx]⟩
   left_inv g := by
     ext
     simp only [comp_apply, liftOfRightInverseAux_comp_apply, Subtype.coe_mk]
diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean
index a0ee1b9441d79..1bf4b67f90258 100644
--- a/Mathlib/Algebra/Group/Submonoid/Operations.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Operations.lean
@@ -865,8 +865,8 @@ that `f x = 1` -/
 def mker (f : F) : Submonoid M :=
   (⊥ : Submonoid N).comap f
 
-@[to_additive]
-theorem mem_mker (f : F) {x : M} : x ∈ mker f ↔ f x = 1 :=
+@[to_additive (attr := simp)]
+theorem mem_mker {f : F} {x : M} : x ∈ mker f ↔ f x = 1 :=
   Iff.rfl
 
 @[to_additive]
@@ -875,7 +875,7 @@ theorem coe_mker (f : F) : (mker f : Set M) = (f : M → N) ⁻¹' {1} :=
 
 @[to_additive]
 instance decidableMemMker [DecidableEq N] (f : F) : DecidablePred (· ∈ mker f) := fun x =>
-  decidable_of_iff (f x = 1) (mem_mker f)
+  decidable_of_iff (f x = 1) mem_mker
 
 @[to_additive]
 theorem comap_mker (g : N →* P) (f : M →* N) : g.mker.comap f = mker (comp g f) :=
diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean
index 3c1f32a790e1d..2fcf4d22646c5 100644
--- a/Mathlib/Algebra/Lie/Submodule.lean
+++ b/Mathlib/Algebra/Lie/Submodule.lean
@@ -1048,6 +1048,7 @@ theorem ker_le_comap : f.ker ≤ J.comap f :=
 theorem ker_coeSubmodule : LieSubmodule.toSubmodule (ker f) = LinearMap.ker (f : L →ₗ[R] L') :=
   rfl
 
+variable {f} in
 @[simp]
 theorem mem_ker {x : L} : x ∈ ker f ↔ f x = 0 :=
   show x ∈ LieSubmodule.toSubmodule (f.ker) ↔ _ by
@@ -1155,9 +1156,12 @@ theorem map_sup_ker_eq_map : LieIdeal.map f (I ⊔ f.ker) = LieIdeal.map f I :=
   suffices LieIdeal.map f (I ⊔ f.ker) ≤ LieIdeal.map f I by
     exact le_antisymm this (LieIdeal.map_mono le_sup_left)
   apply LieSubmodule.lieSpan_mono
-  rintro x ⟨y, hy₁, hy₂⟩; rw [← hy₂]
-  erw [LieSubmodule.mem_sup] at hy₁;obtain ⟨z₁, hz₁, z₂, hz₂, hy⟩ := hy₁; rw [← hy]
-  rw [f.coe_toLinearMap, f.map_add, f.mem_ker.mp hz₂, add_zero]; exact ⟨z₁, hz₁, rfl⟩
+  rintro x ⟨y, hy₁, hy₂⟩
+  rw [← hy₂]
+  erw [LieSubmodule.mem_sup] at hy₁
+  obtain ⟨z₁, hz₁, z₂, hz₂, hy⟩ := hy₁
+  rw [← hy]
+  rw [f.coe_toLinearMap, f.map_add, LieHom.mem_ker.mp hz₂, add_zero]; exact ⟨z₁, hz₁, rfl⟩
 
 @[simp]
 theorem map_sup_ker_eq_map' :
@@ -1249,7 +1253,7 @@ theorem ker_eq_bot : f.ker = ⊥ ↔ Function.Injective f := by
 variable {f}
 
 @[simp]
-theorem mem_ker (m : M) : m ∈ f.ker ↔ f m = 0 :=
+theorem mem_ker {m : M} : m ∈ f.ker ↔ f m = 0 :=
   Iff.rfl
 
 @[simp]
@@ -1257,7 +1261,7 @@ theorem ker_id : (LieModuleHom.id : M →ₗ⁅R,L⁆ M).ker = ⊥ :=
   rfl
 
 @[simp]
-theorem comp_ker_incl : f.comp f.ker.incl = 0 := by ext ⟨m, hm⟩; exact (mem_ker m).mp hm
+theorem comp_ker_incl : f.comp f.ker.incl = 0 := by ext ⟨m, hm⟩; exact mem_ker.mp hm
 
 theorem le_ker_iff_map (M' : LieSubmodule R L M) : M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥ := by
   rw [ker, eq_bot_iff, LieSubmodule.map_le_iff_le_comap]
diff --git a/Mathlib/GroupTheory/Abelianization.lean b/Mathlib/GroupTheory/Abelianization.lean
index 51b0cfca00034..5ee8a835a60c4 100644
--- a/Mathlib/GroupTheory/Abelianization.lean
+++ b/Mathlib/GroupTheory/Abelianization.lean
@@ -125,7 +125,7 @@ theorem commutator_subset_ker : commutator G ≤ f.ker := by
 /-- If `f : G → A` is a group homomorphism to an abelian group, then `lift f` is the unique map
   from the abelianization of a `G` to `A` that factors through `f`. -/
 def lift : (G →* A) ≃ (Abelianization G →* A) where
-  toFun f := QuotientGroup.lift _ f fun _ h => f.mem_ker.2 <| commutator_subset_ker _ h
+  toFun f := QuotientGroup.lift _ f fun _ h => MonoidHom.mem_ker.2 <| commutator_subset_ker _ h
   invFun F := F.comp of
   left_inv _ := MonoidHom.ext fun _ => rfl
   right_inv _ := MonoidHom.ext fun x => QuotientGroup.induction_on x fun _ => rfl
diff --git a/Mathlib/GroupTheory/PresentedGroup.lean b/Mathlib/GroupTheory/PresentedGroup.lean
index 492c52f336a3f..35916a0da95d5 100644
--- a/Mathlib/GroupTheory/PresentedGroup.lean
+++ b/Mathlib/GroupTheory/PresentedGroup.lean
@@ -66,11 +66,11 @@ local notation "F" => FreeGroup.lift f
 
 theorem closure_rels_subset_ker (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
     Subgroup.normalClosure rels ≤ MonoidHom.ker F :=
-  Subgroup.normalClosure_le_normal fun x w ↦ (MonoidHom.mem_ker _).2 (h x w)
+  Subgroup.normalClosure_le_normal fun x w ↦ MonoidHom.mem_ker.2 (h x w)
 
 theorem to_group_eq_one_of_mem_closure (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
     ∀ x ∈ Subgroup.normalClosure rels, F x = 1 :=
-  fun _ w ↦ (MonoidHom.mem_ker _).1 <| closure_rels_subset_ker h w
+  fun _ w ↦ MonoidHom.mem_ker.1 <| closure_rels_subset_ker h w
 
 /-- The extension of a map `f : α → G` that satisfies the given relations to a group homomorphism
 from `PresentedGroup rels → G`. -/
diff --git a/Mathlib/GroupTheory/QuotientGroup/Basic.lean b/Mathlib/GroupTheory/QuotientGroup/Basic.lean
index a2f47594605f9..7857eb080a61d 100644
--- a/Mathlib/GroupTheory/QuotientGroup/Basic.lean
+++ b/Mathlib/GroupTheory/QuotientGroup/Basic.lean
@@ -320,7 +320,7 @@ open MonoidHom
 /-- The induced map from the quotient by the kernel to the codomain. -/
 @[to_additive "The induced map from the quotient by the kernel to the codomain."]
 def kerLift : G ⧸ ker φ →* H :=
-  lift _ φ fun _g => φ.mem_ker.mp
+  lift _ φ fun _g => mem_ker.mp
 
 @[to_additive (attr := simp)]
 theorem kerLift_mk (g : G) : (kerLift φ) g = φ g :=
@@ -340,7 +340,7 @@ theorem kerLift_injective : Injective (kerLift φ) := fun a b =>
 /-- The induced map from the quotient by the kernel to the range. -/
 @[to_additive "The induced map from the quotient by the kernel to the range."]
 def rangeKerLift : G ⧸ ker φ →* φ.range :=
-  lift _ φ.rangeRestrict fun g hg => (mem_ker _).mp <| by rwa [ker_rangeRestrict]
+  lift _ φ.rangeRestrict fun g hg => mem_ker.mp <| by rwa [ker_rangeRestrict]
 
 @[to_additive]
 theorem rangeKerLift_injective : Injective (rangeKerLift φ) := fun a b =>
diff --git a/Mathlib/GroupTheory/Torsion.lean b/Mathlib/GroupTheory/Torsion.lean
index 9e505a267b935..1fe565875fe91 100644
--- a/Mathlib/GroupTheory/Torsion.lean
+++ b/Mathlib/GroupTheory/Torsion.lean
@@ -91,7 +91,7 @@ theorem IsTorsion.of_surjective {f : G →* H} (hf : Function.Surjective f) (tG
 theorem IsTorsion.extension_closed {f : G →* H} (hN : N = f.ker) (tH : IsTorsion H)
     (tN : IsTorsion N) : IsTorsion G := fun g => by
   obtain ⟨ngn, ngnpos, hngn⟩ := (tH <| f g).exists_pow_eq_one
-  have hmem := f.mem_ker.mpr ((f.map_pow g ngn).trans hngn)
+  have hmem := MonoidHom.mem_ker.mpr ((f.map_pow g ngn).trans hngn)
   lift g ^ ngn to N using hN.symm ▸ hmem with gn h
   obtain ⟨nn, nnpos, hnn⟩ := (tN gn).exists_pow_eq_one
   exact isOfFinOrder_iff_pow_eq_one.mpr <| ⟨ngn * nn, mul_pos ngnpos nnpos, by
diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean
index ab874dcea2329..c439259451ff0 100644
--- a/Mathlib/RingTheory/Henselian.lean
+++ b/Mathlib/RingTheory/Henselian.lean
@@ -138,7 +138,7 @@ theorem HenselianLocalRing.TFAE (R : Type u) [CommRing R] [LocalRing R] :
   | hR, K, _K, φ, hφ, f, hf, a₀, h₁, h₂ => by
     obtain ⟨a₀, rfl⟩ := hφ a₀
     have H := HenselianLocalRing.is_henselian f hf a₀
-    simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker φ] at H h₁ h₂
+    simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker] at H h₁ h₂
     obtain ⟨a, ha₁, ha₂⟩ := H h₁ (by
       contrapose! h₂
       rwa [← mem_nonunits_iff, ← LocalRing.mem_maximalIdeal, ← LocalRing.ker_eq_maximalIdeal φ hφ,
diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean
index f26dd00db1d4a..1f4675bf75936 100644
--- a/Mathlib/RingTheory/Ideal/Maps.lean
+++ b/Mathlib/RingTheory/Ideal/Maps.lean
@@ -543,8 +543,9 @@ variable (f : F) (g : G)
 def ker : Ideal R :=
   Ideal.comap f ⊥
 
+variable {f} in
 /-- An element is in the kernel if and only if it maps to zero. -/
-theorem mem_ker {r} : r ∈ ker f ↔ f r = 0 := by rw [ker, Ideal.mem_comap, Submodule.mem_bot]
+@[simp] theorem mem_ker {r} : r ∈ ker f ↔ f r = 0 := by rw [ker, Ideal.mem_comap, Submodule.mem_bot]
 
 theorem ker_eq : (ker f : Set R) = Set.preimage f {0} :=
   rfl
@@ -623,13 +624,13 @@ theorem ker_isMaximal_of_surjective {R K F : Type*} [Ring R] [Field K]
     (hf : Function.Surjective f) : (ker f).IsMaximal := by
   refine
     Ideal.isMaximal_iff.mpr
-      ⟨fun h1 => one_ne_zero' K <| map_one f ▸ (mem_ker f).mp h1, fun J x hJ hxf hxJ => ?_⟩
+      ⟨fun h1 => one_ne_zero' K <| map_one f ▸ mem_ker.mp h1, fun J x hJ hxf hxJ => ?_⟩
   obtain ⟨y, hy⟩ := hf (f x)⁻¹
   have H : 1 = y * x - (y * x - 1) := (sub_sub_cancel _ _).symm
   rw [H]
   refine J.sub_mem (J.mul_mem_left _ hxJ) (hJ ?_)
   rw [mem_ker]
-  simp only [hy, map_sub, map_one, map_mul, inv_mul_cancel₀ (mt (mem_ker f).mpr hxf), sub_self]
+  simp only [hy, map_sub, map_one, map_mul, inv_mul_cancel₀ (mt mem_ker.mpr hxf :), sub_self]
 
 end RingHom
 
@@ -645,7 +646,7 @@ theorem map_eq_bot_iff_le_ker {I : Ideal R} (f : F) : I.map f = ⊥ ↔ I ≤ Ri
   rw [RingHom.ker, eq_bot_iff, map_le_iff_le_comap]
 
 theorem ker_le_comap {K : Ideal S} (f : F) : RingHom.ker f ≤ comap f K := fun _ hx =>
-  mem_comap.2 (((RingHom.mem_ker f).1 hx).symm ▸ K.zero_mem)
+  mem_comap.2 (RingHom.mem_ker.1 hx ▸ K.zero_mem)
 
 theorem map_isPrime_of_equiv {F' : Type*} [EquivLike F' R S] [RingEquivClass F' R S]
     (f : F') {I : Ideal R} [IsPrime I] : IsPrime (map f I) := by
@@ -744,15 +745,15 @@ def liftOfRightInverseAux (hf : Function.RightInverse f_inv f) (g : A →+* C)
   { AddMonoidHom.liftOfRightInverse f.toAddMonoidHom f_inv hf ⟨g.toAddMonoidHom, hg⟩ with
     toFun := fun b => g (f_inv b)
     map_one' := by
-      rw [← map_one g, ← sub_eq_zero, ← map_sub g, ← mem_ker g]
+      rw [← map_one g, ← sub_eq_zero, ← map_sub g, ← mem_ker]
       apply hg
-      rw [mem_ker f, map_sub f, sub_eq_zero, map_one f]
+      rw [mem_ker, map_sub f, sub_eq_zero, map_one f]
       exact hf 1
     map_mul' := by
       intro x y
-      rw [← map_mul g, ← sub_eq_zero, ← map_sub g, ← mem_ker g]
+      rw [← map_mul g, ← sub_eq_zero, ← map_sub g, ← mem_ker]
       apply hg
-      rw [mem_ker f, map_sub f, sub_eq_zero, map_mul f]
+      rw [mem_ker, map_sub f, sub_eq_zero, map_mul f]
       simp only [hf _] }
 
 @[simp]
@@ -782,7 +783,7 @@ See `RingHom.eq_liftOfRightInverse` for the uniqueness lemma.
 def liftOfRightInverse (hf : Function.RightInverse f_inv f) :
     { g : A →+* C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C) where
   toFun g := f.liftOfRightInverseAux f_inv hf g.1 g.2
-  invFun φ := ⟨φ.comp f, fun x hx => (mem_ker _).mpr <| by simp [(mem_ker _).mp hx]⟩
+  invFun φ := ⟨φ.comp f, fun x hx => mem_ker.mpr <| by simp [mem_ker.mp hx]⟩
   left_inv g := by
     ext
     simp only [comp_apply, liftOfRightInverseAux_comp_apply, Subtype.coe_mk]
diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
index 7abf1424f8ab5..5fb624f6f2143 100644
--- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean
+++ b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
@@ -36,7 +36,7 @@ This is an isomorphism if `f` has a right inverse (`quotientKerEquivOfRightInver
 is surjective (`quotientKerEquivOfSurjective`).
 -/
 def kerLift : R ⧸ ker f →+* S :=
-  Ideal.Quotient.lift _ f fun _ => f.mem_ker.mp
+  Ideal.Quotient.lift _ f fun _ => mem_ker.mp
 
 @[simp]
 theorem kerLift_mk (r : R) : kerLift f (Ideal.Quotient.mk (ker f) r) = f r :=
@@ -49,7 +49,7 @@ theorem lift_injective_of_ker_le_ideal (I : Ideal R) {f : R →+* S} (H : ∀ a
   obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective u
   rw [Ideal.Quotient.lift_mk] at hu
   rw [Ideal.Quotient.eq_zero_iff_mem]
-  exact hI ((RingHom.mem_ker f).mpr hu)
+  exact hI (RingHom.mem_ker.mpr hu)
 
 /-- The induced map from the quotient by the kernel is injective. -/
 theorem kerLift_injective : Function.Injective (kerLift f) :=
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 03e036aa35719..1b153b9e33498 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -121,10 +121,10 @@ theorem subsingleton (h : IsAdjoinRoot S f) [Subsingleton R] : Subsingleton S :=
 theorem algebraMap_apply (h : IsAdjoinRoot S f) (x : R) :
     algebraMap R S x = h.map (Polynomial.C x) := by rw [h.algebraMap_eq, RingHom.comp_apply]
 
-@[simp]
 theorem mem_ker_map (h : IsAdjoinRoot S f) {p} : p ∈ RingHom.ker h.map ↔ f ∣ p := by
   rw [h.ker_map, Ideal.mem_span_singleton]
 
+@[simp]
 theorem map_eq_zero_iff (h : IsAdjoinRoot S f) {p} : h.map p = 0 ↔ f ∣ p := by
   rw [← h.mem_ker_map, RingHom.mem_ker]
 
diff --git a/Mathlib/RingTheory/Kaehler/Basic.lean b/Mathlib/RingTheory/Kaehler/Basic.lean
index 4c0d923b7ddfc..09bc7c6dc0c45 100644
--- a/Mathlib/RingTheory/Kaehler/Basic.lean
+++ b/Mathlib/RingTheory/Kaehler/Basic.lean
@@ -808,7 +808,7 @@ def KaehlerDifferential.kerToTensor :
   map_add' x y := by simp only [Submodule.coe_add, map_add, TensorProduct.tmul_add]
   map_smul' r x := by simp only [SetLike.val_smul, smul_eq_mul, Derivation.leibniz,
     TensorProduct.tmul_add, TensorProduct.tmul_smul, TensorProduct.smul_tmul', ←
-    algebraMap_eq_smul_one, (RingHom.mem_ker _).mp x.prop, TensorProduct.zero_tmul, add_zero,
+    algebraMap_eq_smul_one, RingHom.mem_ker.mp x.prop, TensorProduct.zero_tmul, add_zero,
     RingHom.id_apply]
 
 /-- The map `I/I² → B ⊗[A] B ⊗[A] Ω[A⁄R]` where `I = ker(A → B)`. -/
@@ -820,7 +820,7 @@ def KaehlerDifferential.kerCotangentToTensor :
     rintro x hx y -
     simp only [Submodule.mem_comap, LinearMap.lsmul_apply, LinearMap.mem_ker, map_smul,
       kerToTensor_apply, TensorProduct.smul_tmul', ← algebraMap_eq_smul_one,
-      (RingHom.mem_ker _).mp hx, TensorProduct.zero_tmul]))
+      RingHom.mem_ker.mp hx, TensorProduct.zero_tmul]))
 
 @[simp]
 lemma KaehlerDifferential.kerCotangentToTensor_toCotangent (x) :
@@ -837,7 +837,7 @@ theorem KaehlerDifferential.range_kerCotangentToTensor
   constructor
   · rintro ⟨x, rfl⟩
     obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
-    simp [kerCotangentToTensor_toCotangent, (RingHom.mem_ker _).mp x.2]
+    simp [kerCotangentToTensor_toCotangent, RingHom.mem_ker.mp x.2]
   · intro hx
     obtain ⟨x, rfl⟩ := LinearMap.rTensor_surjective (Ω[A⁄R]) (g := Algebra.linearMap A B) h x
     obtain ⟨x, rfl⟩ := (TensorProduct.lid _ _).symm.surjective x
@@ -870,7 +870,7 @@ theorem KaehlerDifferential.range_kerCotangentToTensor
       simp only [smul_sub, TensorProduct.tmul_sub, Finset.sum_sub_distrib, ← TensorProduct.tmul_sum,
         ← Finset.sum_smul, Finset.sum_attach, sub_eq_self,
         Finset.sum_attach (f := fun i ↦ x i • KaehlerDifferential.D R A i)]
-      rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, (RingHom.mem_ker _).mp this,
+      rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
         TensorProduct.zero_tmul]
 
 theorem KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange
diff --git a/Mathlib/RingTheory/Localization/Algebra.lean b/Mathlib/RingTheory/Localization/Algebra.lean
index b92decb0ad796..794c17c9aea4a 100644
--- a/Mathlib/RingTheory/Localization/Algebra.lean
+++ b/Mathlib/RingTheory/Localization/Algebra.lean
@@ -56,7 +56,7 @@ variable (S) in
 /-- The canonical linear map from the kernel of `g` to the kernel of its localization. -/
 def RingHom.toKerIsLocalization (hy : M ≤ Submonoid.comap g T) :
     RingHom.ker g →ₗ[R] RingHom.ker (IsLocalization.map Q g hy : S →+* Q) where
-  toFun x := ⟨algebraMap R S x, by simp [RingHom.mem_ker, (RingHom.mem_ker g).mp x.property]⟩
+  toFun x := ⟨algebraMap R S x, by simp [RingHom.mem_ker, RingHom.mem_ker.mp x.property]⟩
   map_add' x y := by
     simp only [Submodule.coe_add, map_add, AddMemClass.mk_add_mk]
   map_smul' a x := by
diff --git a/Mathlib/RingTheory/Polynomial/Basic.lean b/Mathlib/RingTheory/Polynomial/Basic.lean
index fe44dfcd045fe..ab6d03ba20af2 100644
--- a/Mathlib/RingTheory/Polynomial/Basic.lean
+++ b/Mathlib/RingTheory/Polynomial/Basic.lean
@@ -605,8 +605,7 @@ theorem _root_.Polynomial.ker_mapRingHom (f : R →+* S) :
   ext
   simp only [LinearMap.mem_ker, RingHom.toSemilinearMap_apply, coe_mapRingHom]
   rw [mem_map_C_iff, Polynomial.ext_iff]
-  simp_rw [RingHom.mem_ker f]
-  simp
+  simp [RingHom.mem_ker]
 
 variable (I : Ideal R[X])
 
diff --git a/Mathlib/RingTheory/Smooth/Kaehler.lean b/Mathlib/RingTheory/Smooth/Kaehler.lean
index 0e20b7e631d12..e11be1b55e317 100644
--- a/Mathlib/RingTheory/Smooth/Kaehler.lean
+++ b/Mathlib/RingTheory/Smooth/Kaehler.lean
@@ -112,7 +112,7 @@ lemma retractionOfSectionOfKerSqZero_tmul_D (s : S) (t : P) :
 
 lemma retractionOfSectionOfKerSqZero_comp_kerToTensor :
     (retractionOfSectionOfKerSqZero g hf' hg).comp (kerToTensor R P S) = LinearMap.id := by
-  ext x; simp [(RingHom.mem_ker _).mp x.2]
+  ext x; simp [RingHom.mem_ker.mp x.2]
 
 end ofSection
 
@@ -172,7 +172,7 @@ lemma toAlgHom_comp_sectionOfRetractionKerToTensorAux :
       (sectionOfRetractionKerToTensorAux l hl σ hσ hf') = AlgHom.id _ _ := by
   ext x
   obtain ⟨x, rfl⟩ := hf x
-  simp [sectionOfRetractionKerToTensorAux_algebraMap, (RingHom.mem_ker _).mp]
+  simp [sectionOfRetractionKerToTensorAux_algebraMap, RingHom.mem_ker.mp]
 
 /--
 Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`.