diff --git a/Mathlib.lean b/Mathlib.lean
index 910c87e9c8dfb..1d5793498fbc1 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -270,6 +270,7 @@ import Mathlib.Algebra.Group.Action.Defs
 import Mathlib.Algebra.Group.Action.End
 import Mathlib.Algebra.Group.Action.Equidecomp
 import Mathlib.Algebra.Group.Action.Faithful
+import Mathlib.Algebra.Group.Action.Hom
 import Mathlib.Algebra.Group.Action.Opposite
 import Mathlib.Algebra.Group.Action.Option
 import Mathlib.Algebra.Group.Action.Pi
diff --git a/Mathlib/Algebra/AddConstMap/Basic.lean b/Mathlib/Algebra/AddConstMap/Basic.lean
index 1f7087d7e049d..f0ab3407e159e 100644
--- a/Mathlib/Algebra/AddConstMap/Basic.lean
+++ b/Mathlib/Algebra/AddConstMap/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import Mathlib.Algebra.Group.Action.End
 import Mathlib.Algebra.Group.Action.Pi
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.Module.NatInt
diff --git a/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean b/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
index 0bc4ab7b5af97..a62346a282427 100644
--- a/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
+++ b/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
@@ -4,10 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.Finprod
-import Mathlib.Algebra.BigOperators.Group.Finset.Basic
-import Mathlib.Algebra.GroupWithZero.Action.Defs
-import Mathlib.Algebra.Order.Group.Multiset
-import Mathlib.Data.Finset.Basic
+import Mathlib.Algebra.Group.Action.Basic
 
 /-!
 # Lemmas about group actions on big operators
diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
index fa3ae76a99db8..7a49ab8e3f84c 100644
--- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -564,8 +564,8 @@ protected def counit' : coextendScalars f ⋙ restrictScalars f ⟶ 𝟭 (Module
         dsimp
         rw [CoextendScalars.smul_apply, one_mul, ← LinearMap.map_smul]
         congr
-        change f r = (f r) • (1 : S)
-        rw [smul_eq_mul (a := f r) (a' := 1), mul_one] }
+        change f r = f r • (1 : S)
+        rw [smul_eq_mul (f r) 1, mul_one] }
 
 end RestrictionCoextensionAdj
 
diff --git a/Mathlib/Algebra/GradedMonoid.lean b/Mathlib/Algebra/GradedMonoid.lean
index fdd30ae85747a..2fe57b47d0d9f 100644
--- a/Mathlib/Algebra/GradedMonoid.lean
+++ b/Mathlib/Algebra/GradedMonoid.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.BigOperators.Group.List.Lemmas
-import Mathlib.Algebra.Group.Action.End
+import Mathlib.Algebra.Group.Action.Hom
 import Mathlib.Algebra.Group.Submonoid.Defs
 import Mathlib.Data.List.FinRange
 import Mathlib.Data.SetLike.Basic
diff --git a/Mathlib/Algebra/Group/Action/Basic.lean b/Mathlib/Algebra/Group/Action/Basic.lean
index 0077326ec936b..812ad9d9894c0 100644
--- a/Mathlib/Algebra/Group/Action/Basic.lean
+++ b/Mathlib/Algebra/Group/Action/Basic.lean
@@ -5,7 +5,6 @@ Authors: Chris Hughes
 -/
 import Mathlib.Algebra.Group.Action.Units
 import Mathlib.Algebra.Group.Invertible.Basic
-import Mathlib.GroupTheory.Perm.Basic
 
 /-!
 # More lemmas about group actions
@@ -16,7 +15,7 @@ This file contains lemmas about group actions that require more imports than
 
 assert_not_exists MonoidWithZero
 
-variable {α β : Type*}
+variable {M N α β : Type*}
 
 section MulAction
 
@@ -38,21 +37,54 @@ lemma MulAction.toPerm_injective [FaithfulSMul α β] :
     Function.Injective (MulAction.toPerm : α → Equiv.Perm β) :=
   (show Function.Injective (Equiv.toFun ∘ MulAction.toPerm) from smul_left_injective').of_comp
 
-variable (α) (β)
+section
+variable [Monoid M] [MulAction M α]
+
+/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.
+
+See also `Function.Surjective.distribMulActionLeft` and `Function.Surjective.moduleLeft`.
+-/
+@[to_additive
+"Push forward the action of `R` on `M` along a compatible surjective map `f : R →+ S`."]
+abbrev Function.Surjective.mulActionLeft {R S M : Type*} [Monoid R] [MulAction R M] [Monoid S]
+    [SMul S M] (f : R →* S) (hf : Surjective f) (hsmul : ∀ (c) (x : M), f c • x = c • x) :
+    MulAction S M where
+  smul := (· • ·)
+  one_smul b := by rw [← f.map_one, hsmul, one_smul]
+  mul_smul := hf.forall₂.mpr fun a b x ↦ by simp only [← f.map_mul, hsmul, mul_smul]
+
+namespace MulAction
+
+variable (α)
+
+/-- A multiplicative action of `M` on `α` and a monoid homomorphism `N → M` induce
+a multiplicative action of `N` on `α`.
+
+See note [reducible non-instances]. -/
+@[to_additive]
+abbrev compHom [Monoid N] (g : N →* M) : MulAction N α where
+  smul := SMul.comp.smul g
+  -- Porting note: was `by simp [g.map_one, MulAction.one_smul]`
+  one_smul _ := by simpa [(· • ·)] using MulAction.one_smul ..
+  -- Porting note: was `by simp [g.map_mul, MulAction.mul_smul]`
+  mul_smul _ _ _ := by simpa [(· • ·)] using MulAction.mul_smul ..
+
+/-- An additive action of `M` on `α` and an additive monoid homomorphism `N → M` induce
+an additive action of `N` on `α`.
+
+See note [reducible non-instances]. -/
+add_decl_doc AddAction.compHom
+
+@[to_additive]
+lemma compHom_smul_def
+    {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) :
+    letI : MulAction E G := MulAction.compHom _ f
+    a • x = (f a) • x := rfl
+
+end MulAction
+end
 
-/-- Given an action of a group `α` on a set `β`, each `g : α` defines a permutation of `β`. -/
-@[simps]
-def MulAction.toPermHom : α →* Equiv.Perm β where
-  toFun := MulAction.toPerm
-  map_one' := Equiv.ext <| one_smul α
-  map_mul' u₁ u₂ := Equiv.ext <| mul_smul (u₁ : α) u₂
-
-/-- Given an action of an additive group `α` on a set `β`, each `g : α` defines a permutation of
-`β`. -/
-@[simps!]
-def AddAction.toPermHom (α : Type*) [AddGroup α] [AddAction α β] :
-    α →+ Additive (Equiv.Perm β) :=
-  MonoidHom.toAdditive'' <| MulAction.toPermHom (Multiplicative α) β
+variable (α) (β)
 
 /-- The tautological action by `Equiv.Perm α` on `α`.
 
diff --git a/Mathlib/Algebra/Group/Action/Defs.lean b/Mathlib/Algebra/Group/Action/Defs.lean
index 3ca41ad778aa4..fd71d46016cc3 100644
--- a/Mathlib/Algebra/Group/Action/Defs.lean
+++ b/Mathlib/Algebra/Group/Action/Defs.lean
@@ -57,8 +57,23 @@ variable {M N G H α β γ δ : Type*}
 @[to_additive "See also `AddMonoid.toAddAction`"]
 instance (priority := 910) Mul.toSMul (α : Type*) [Mul α] : SMul α α := ⟨(· * ·)⟩
 
+/-- Like `Mul.toSMul`, but multiplies on the right.
+
+See also `Monoid.toOppositeMulAction` and `MonoidWithZero.toOppositeMulActionWithZero`. -/
+@[to_additive "Like `Add.toVAdd`, but adds on the right.
+
+  See also `AddMonoid.toOppositeAddAction`."]
+instance (priority := 910) Mul.toSMulMulOpposite (α : Type*) [Mul α] : SMul αᵐᵒᵖ α where
+  smul a b := b * a.unop
+
+@[to_additive (attr := simp)]
+lemma smul_eq_mul {α : Type*} [Mul α] (a b : α) : a • b = a * b := rfl
+
+@[to_additive]
+lemma op_smul_eq_mul {α : Type*} [Mul α] (a b : α) : MulOpposite.op a • b = b * a := rfl
+
 @[to_additive (attr := simp)]
-lemma smul_eq_mul (α : Type*) [Mul α] {a a' : α} : a • a' = a * a' := rfl
+lemma MulOpposite.smul_eq_mul_unop [Mul α] (a : αᵐᵒᵖ) (b : α) : a • b = b * a.unop := rfl
 
 /-- Type class for additive monoid actions. -/
 class AddAction (G : Type*) (P : Type*) [AddMonoid G] extends VAdd G P where
@@ -485,3 +500,22 @@ lemma SMulCommClass.of_mul_smul_one {M N} [Monoid N] [SMul M N]
   ⟨fun x y z ↦ by rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]⟩
 
 end CompatibleScalar
+
+/-- Typeclass for multiplicative actions on multiplicative structures. This generalizes
+conjugation actions. -/
+@[ext]
+class MulDistribMulAction (M N : Type*) [Monoid M] [Monoid N] extends MulAction M N where
+  /-- Distributivity of `•` across `*` -/
+  smul_mul : ∀ (r : M) (x y : N), r • (x * y) = r • x * r • y
+  /-- Multiplying `1` by a scalar gives `1` -/
+  smul_one : ∀ r : M, r • (1 : N) = 1
+
+export MulDistribMulAction (smul_one)
+
+section MulDistribMulAction
+variable [Monoid M] [Monoid N] [MulDistribMulAction M N]
+
+lemma smul_mul' (a : M) (b₁ b₂ : N) : a • (b₁ * b₂) = a • b₁ * a • b₂ :=
+  MulDistribMulAction.smul_mul ..
+
+end MulDistribMulAction
diff --git a/Mathlib/Algebra/Group/Action/End.lean b/Mathlib/Algebra/Group/Action/End.lean
index cc56cc2c6fc66..f9e9897316ec9 100644
--- a/Mathlib/Algebra/Group/Action/End.lean
+++ b/Mathlib/Algebra/Group/Action/End.lean
@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Action.Defs
+import Mathlib.Algebra.Group.Equiv.Defs
 import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.GroupTheory.Perm.Basic
 
 /-!
 # Endomorphisms, homomorphisms and group actions
@@ -31,52 +33,7 @@ assert_not_exists MonoidWithZero
 
 open Function (Injective Surjective)
 
-variable {M N α : Type*}
-
-section
-variable [Monoid M] [MulAction M α]
-
-/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.
-
-See also `Function.Surjective.distribMulActionLeft` and `Function.Surjective.moduleLeft`.
--/
-@[to_additive
-"Push forward the action of `R` on `M` along a compatible surjective map `f : R →+ S`."]
-abbrev Function.Surjective.mulActionLeft {R S M : Type*} [Monoid R] [MulAction R M] [Monoid S]
-    [SMul S M] (f : R →* S) (hf : Surjective f) (hsmul : ∀ (c) (x : M), f c • x = c • x) :
-    MulAction S M where
-  smul := (· • ·)
-  one_smul b := by rw [← f.map_one, hsmul, one_smul]
-  mul_smul := hf.forall₂.mpr fun a b x ↦ by simp only [← f.map_mul, hsmul, mul_smul]
-
-namespace MulAction
-
-variable (α)
-
-/-- A multiplicative action of `M` on `α` and a monoid homomorphism `N → M` induce
-a multiplicative action of `N` on `α`.
-
-See note [reducible non-instances]. -/
-@[to_additive]
-abbrev compHom [Monoid N] (g : N →* M) : MulAction N α where
-  smul := SMul.comp.smul g
-  one_smul _ := by simpa [(· • ·)] using MulAction.one_smul ..
-  mul_smul _ _ _ := by simpa [(· • ·)] using MulAction.mul_smul ..
-
-/-- An additive action of `M` on `α` and an additive monoid homomorphism `N → M` induce
-an additive action of `N` on `α`.
-
-See note [reducible non-instances]. -/
-add_decl_doc AddAction.compHom
-
-@[to_additive]
-lemma compHom_smul_def
-    {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) :
-    letI : MulAction E G := MulAction.compHom _ f
-    a • x = (f a) • x := rfl
-
-end MulAction
-end
+variable {G M N O α : Type*}
 
 section CompatibleScalar
 
@@ -105,8 +62,7 @@ def monoidHomEquivMulActionIsScalarTower (M N) [Monoid M] [Monoid N] :
 
 end CompatibleScalar
 
-variable (α)
-
+variable (α) in
 /-- The monoid of endomorphisms.
 
 Note that this is generalized by `CategoryTheory.End` to categories other than `Type u`. -/
@@ -123,8 +79,6 @@ instance : Monoid (Function.End α) where
 
 instance : Inhabited (Function.End α) := ⟨1⟩
 
-variable {α}
-
 /-- The tautological action by `Function.End α` on `α`.
 
 This is generalized to bundled endomorphisms by:
@@ -144,6 +98,9 @@ instance Function.End.applyMulAction : MulAction (Function.End α) α where
   one_smul _ := rfl
   mul_smul _ _ _ := rfl
 
+/-- The tautological additive action by `Additive (Function.End α)` on `α`. -/
+instance Function.End.applyAddAction : AddAction (Additive (Function.End α)) α := inferInstance
+
 @[simp] lemma Function.End.smul_def (f : Function.End α) (a : α) : f • a = f a := rfl
 
 --TODO - This statement should be somethting like `toFun (f * g) = toFun f ∘ toFun g`
@@ -152,6 +109,10 @@ lemma Function.End.mul_def (f g : Function.End α) : (f * g) = f ∘ g := rfl
 --TODO - This statement should be somethting like `toFun 1 = id`
 lemma Function.End.one_def : (1 : Function.End α) = id := rfl
 
+/-- `Function.End.applyMulAction` is faithful. -/
+instance Function.End.apply_FaithfulSMul : FaithfulSMul (Function.End α) α where
+  eq_of_smul_eq_smul := funext
+
 /-- The monoid hom representing a monoid action.
 
 When `M` is a group, see `MulAction.toPermHom`. -/
@@ -160,8 +121,88 @@ def MulAction.toEndHom [Monoid M] [MulAction M α] : M →* Function.End α wher
   map_one' := funext (one_smul M)
   map_mul' x y := funext (mul_smul x y)
 
+/-- The additive monoid hom representing an additive monoid action.
+
+When `M` is a group, see `AddAction.toPermHom`. -/
+def AddAction.toEndHom [AddMonoid M] [AddAction M α] : M →+ Additive (Function.End α) :=
+  MonoidHom.toAdditive'' MulAction.toEndHom
+
 /-- The monoid action induced by a monoid hom to `Function.End α`
 
 See note [reducible non-instances]. -/
-abbrev MulAction.ofEndHom [Monoid M] (f : M →* Function.End α) : MulAction M α :=
-  MulAction.compHom α f
+abbrev MulAction.ofEndHom [Monoid M] (f : M →* Function.End α) : MulAction M α := .compHom α f
+
+/-- Given an action of an additive group `α` on a set `β`, each `g : α` defines a permutation of
+`β`. -/
+@[simps!]
+def AddAction.toPermHom (α : Type*) [AddGroup α] [AddAction α β] :
+    α →+ Additive (Equiv.Perm β) :=
+  MonoidHom.toAdditive'' <| MulAction.toPermHom (Multiplicative α) β
+
+/-- Given an action of a group `G` on a type `α`, each `g : G` defines a permutation of `α`. -/
+@[simps]
+def MulAction.toPermHom [Group G] [MulAction G α] : G →* Equiv.Perm α where
+  toFun := MulAction.toPerm
+  map_one' := Equiv.ext <| one_smul α
+  map_mul' u₁ u₂ := Equiv.ext <| mul_smul (u₁ : α) u₂
+
+section MulDistribMulAction
+variable [Monoid M] [Monoid N] [Monoid O] [MulDistribMulAction M N] [MulDistribMulAction N O]
+
+/-- Pullback a multiplicative distributive multiplicative action along an injective monoid
+homomorphism.
+See note [reducible non-instances]. -/
+protected abbrev Function.Injective.mulDistribMulAction [SMul M O] (f : O →* N) (hf : Injective f)
+  (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulDistribMulAction M O where
+  __ := hf.mulAction f smul
+  smul_mul c x y := hf <| by simp only [smul, f.map_mul, smul_mul']
+  smul_one c := hf <| by simp only [smul, f.map_one, smul_one]
+
+/-- Pushforward a multiplicative distributive multiplicative action along a surjective monoid
+homomorphism.
+See note [reducible non-instances]. -/
+protected abbrev Function.Surjective.mulDistribMulAction [SMul M O] (f : N →* O) (hf : Surjective f)
+    (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulDistribMulAction M O where
+  __ := hf.mulAction f smul
+  smul_mul c := by simp only [hf.forall, smul_mul', ← smul, ← f.map_mul, implies_true]
+  smul_one c := by rw [← f.map_one, ← smul, smul_one]
+
+variable (N) in
+/-- Scalar multiplication by `r` as a `MonoidHom`. -/
+def MulDistribMulAction.toMonoidHom (r : M) : N →* N where
+  toFun := (r • ·)
+  map_one' := smul_one r
+  map_mul' := smul_mul' r
+
+@[simp]
+lemma MulDistribMulAction.toMonoidHom_apply (r : M) (x : N) : toMonoidHom N r x = r • x := rfl
+
+@[simp] lemma smul_pow' (r : M) (x : N) (n : ℕ) : r • x ^ n = (r • x) ^ n :=
+  (MulDistribMulAction.toMonoidHom ..).map_pow ..
+
+end MulDistribMulAction
+
+section MulDistribMulAction
+variable [Monoid M] [Group G] [MulDistribMulAction M G]
+
+@[simp]
+lemma smul_inv' (r : M) (x : G) : r • x⁻¹ = (r • x)⁻¹ :=
+  (MulDistribMulAction.toMonoidHom G r).map_inv x
+
+lemma smul_div' (r : M) (x y : G) : r • (x / y) = r • x / r • y :=
+  map_div (MulDistribMulAction.toMonoidHom G r) x y
+
+end MulDistribMulAction
+
+section MulDistribMulAction
+variable [Group G] [Monoid M] [MulDistribMulAction G M]
+variable (M)
+
+/-- Each element of the group defines a multiplicative monoid isomorphism.
+
+This is a stronger version of `MulAction.toPerm`. -/
+@[simps (config := { simpRhs := true })]
+def MulDistribMulAction.toMulEquiv (x : G) : M ≃* M :=
+  { MulDistribMulAction.toMonoidHom M x, MulAction.toPermHom G M x with }
+
+end MulDistribMulAction
diff --git a/Mathlib/Algebra/Group/Action/Faithful.lean b/Mathlib/Algebra/Group/Action/Faithful.lean
index 7fc8304636a27..162c491acb222 100644
--- a/Mathlib/Algebra/Group/Action/Faithful.lean
+++ b/Mathlib/Algebra/Group/Action/Faithful.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yury Kudryashov
 -/
-import Mathlib.Algebra.Group.Action.End
+import Mathlib.Algebra.Group.Action.Defs
 
 /-!
 # Faithful group actions
@@ -53,9 +53,10 @@ lemma smul_left_injective' [SMul M α] [FaithfulSMul M α] : Injective ((· •
 
 /-- `Monoid.toMulAction` is faithful on cancellative monoids. -/
 @[to_additive " `AddMonoid.toAddAction` is faithful on additive cancellative monoids. "]
-instance RightCancelMonoid.faithfulSMul [RightCancelMonoid α] : FaithfulSMul α α :=
+instance RightCancelMonoid.to_faithfulSMul [RightCancelMonoid α] : FaithfulSMul α α :=
   ⟨fun h ↦ mul_right_cancel (h 1)⟩
 
-/-- `Function.End.applyMulAction` is faithful. -/
-instance Function.End.apply_FaithfulSMul : FaithfulSMul (Function.End α) α :=
-  ⟨fun {_ _} ↦ funext⟩
+/-- `Monoid.toOppositeMulAction` is faithful on cancellative monoids. -/
+@[to_additive " `AddMonoid.toOppositeAddAction` is faithful on additive cancellative monoids. "]
+instance LefttCancelMonoid.to_faithfulSMul_mulOpposite [LeftCancelMonoid α] : FaithfulSMul αᵐᵒᵖ α :=
+  ⟨fun h ↦ MulOpposite.unop_injective <| mul_left_cancel (h 1)⟩
diff --git a/Mathlib/Algebra/Group/Action/Hom.lean b/Mathlib/Algebra/Group/Action/Hom.lean
new file mode 100644
index 0000000000000..2383ebf23e12e
--- /dev/null
+++ b/Mathlib/Algebra/Group/Action/Hom.lean
@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Yury Kudryashov
+-/
+import Mathlib.Algebra.Group.Action.Pretransitive
+import Mathlib.Algebra.Group.Hom.Defs
+
+/-!
+# Homomorphisms and group actions
+-/
+
+assert_not_exists MonoidWithZero
+
+open Function (Injective Surjective)
+
+variable {M N α : Type*}
+
+section
+variable [Monoid M] [MulAction M α]
+
+/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.
+
+See also `Function.Surjective.distribMulActionLeft` and `Function.Surjective.moduleLeft`.
+-/
+@[to_additive
+"Push forward the action of `R` on `M` along a compatible surjective map `f : R →+ S`."]
+abbrev Function.Surjective.mulActionLeft {R S M : Type*} [Monoid R] [MulAction R M] [Monoid S]
+    [SMul S M] (f : R →* S) (hf : Surjective f) (hsmul : ∀ (c) (x : M), f c • x = c • x) :
+    MulAction S M where
+  smul := (· • ·)
+  one_smul b := by rw [← f.map_one, hsmul, one_smul]
+  mul_smul := hf.forall₂.mpr fun a b x ↦ by simp only [← f.map_mul, hsmul, mul_smul]
+
+namespace MulAction
+
+variable (α)
+
+/-- A multiplicative action of `M` on `α` and a monoid homomorphism `N → M` induce
+a multiplicative action of `N` on `α`.
+
+See note [reducible non-instances]. -/
+@[to_additive]
+abbrev compHom [Monoid N] (g : N →* M) : MulAction N α where
+  smul := SMul.comp.smul g
+  one_smul _ := by simpa [(· • ·)] using MulAction.one_smul ..
+  mul_smul _ _ _ := by simpa [(· • ·)] using MulAction.mul_smul ..
+
+/-- An additive action of `M` on `α` and an additive monoid homomorphism `N → M` induce
+an additive action of `N` on `α`.
+
+See note [reducible non-instances]. -/
+add_decl_doc AddAction.compHom
+
+@[to_additive]
+lemma compHom_smul_def
+    {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) :
+    letI : MulAction E G := MulAction.compHom _ f
+    a • x = (f a) • x := rfl
+
+/-- If an action is transitive, then composing this action with a surjective homomorphism gives
+again a transitive action. -/
+@[to_additive]
+lemma isPretransitive_compHom {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G]
+    [IsPretransitive F G] {f : E →* F} (hf : Surjective f) :
+    letI : MulAction E G := MulAction.compHom _ f
+    IsPretransitive E G := by
+  let _ : MulAction E G := MulAction.compHom _ f
+  refine ⟨fun x y ↦ ?_⟩
+  obtain ⟨m, rfl⟩ : ∃ m : F, m • x = y := exists_smul_eq F x y
+  obtain ⟨e, rfl⟩ : ∃ e, f e = m := hf m
+  exact ⟨e, rfl⟩
+
+@[to_additive]
+lemma IsPretransitive.of_compHom {M N α : Type*} [Monoid M] [Monoid N] [MulAction N α]
+    (f : M →* N) [h : letI := compHom α f; IsPretransitive M α] : IsPretransitive N α :=
+  letI := compHom α f; h.of_smul_eq f rfl
+
+end MulAction
+end
+
+section CompatibleScalar
+
+/-- If the multiplicative action of `M` on `N` is compatible with multiplication on `N`, then
+`fun x ↦ x • 1` is a monoid homomorphism from `M` to `N`. -/
+@[to_additive (attr := simps)
+"If the additive action of `M` on `N` is compatible with addition on `N`, then
+`fun x ↦ x +ᵥ 0` is an additive monoid homomorphism from `M` to `N`."]
+def MonoidHom.smulOneHom {M N} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] :
+    M →* N where
+  toFun x := x • (1 : N)
+  map_one' := one_smul _ _
+  map_mul' x y := by rw [smul_one_mul, smul_smul]
+
+/-- A monoid homomorphism between two monoids M and N can be equivalently specified by a
+multiplicative action of M on N that is compatible with the multiplication on N. -/
+@[to_additive
+"A monoid homomorphism between two additive monoids M and N can be equivalently
+specified by an additive action of M on N that is compatible with the addition on N."]
+def monoidHomEquivMulActionIsScalarTower (M N) [Monoid M] [Monoid N] :
+    (M →* N) ≃ {_inst : MulAction M N // IsScalarTower M N N} where
+  toFun f := ⟨MulAction.compHom N f, SMul.comp.isScalarTower _⟩
+  invFun := fun ⟨_, _⟩ ↦ MonoidHom.smulOneHom
+  left_inv f := MonoidHom.ext fun m ↦ mul_one (f m)
+  right_inv := fun ⟨_, _⟩ ↦ Subtype.ext <| MulAction.ext <| funext₂ <| smul_one_smul N
+
+end CompatibleScalar
diff --git a/Mathlib/Algebra/Group/Action/Opposite.lean b/Mathlib/Algebra/Group/Action/Opposite.lean
index cd669c1f44543..c7ad61287c09b 100644
--- a/Mathlib/Algebra/Group/Action/Opposite.lean
+++ b/Mathlib/Algebra/Group/Action/Opposite.lean
@@ -137,28 +137,10 @@ lemma op_smul_mul (b : β) (a₁ a₂ : α) : b <• (a₁ * a₂) = b <• a₁
 
 end
 
-/-! ### Actions _by_ the opposite type (right actions)
-
-In `Mul.toSMul` in another file, we define the left action `a₁ • a₂ = a₁ * a₂`. For the
-multiplicative opposite, we define `MulOpposite.op a₁ • a₂ = a₂ * a₁`, with the multiplication
-reversed.
--/
+/-! ### Actions _by_ the opposite type (right actions) -/
 
 open MulOpposite
 
-/-- Like `Mul.toSMul`, but multiplies on the right.
-
-See also `Monoid.toOppositeMulAction` and `MonoidWithZero.toOppositeMulActionWithZero`. -/
-@[to_additive "Like `Add.toVAdd`, but adds on the right.
-
-  See also `AddMonoid.toOppositeAddAction`."]
-instance Mul.toHasOppositeSMul [Mul α] : SMul αᵐᵒᵖ α where smul c x := x * c.unop
-
-@[to_additive] lemma op_smul_eq_mul [Mul α] {a a' : α} : op a • a' = a' * a := rfl
-
-@[to_additive (attr := simp)]
-lemma MulOpposite.smul_eq_mul_unop [Mul α] {a : αᵐᵒᵖ} {a' : α} : a • a' = a' * a.unop := rfl
-
 /-- The right regular action of a group on itself is transitive. -/
 @[to_additive "The right regular action of an additive group on itself is transitive."]
 instance MulAction.OppositeRegular.isPretransitive {G : Type*} [Group G] : IsPretransitive Gᵐᵒᵖ G :=
diff --git a/Mathlib/Algebra/Group/Action/Pi.lean b/Mathlib/Algebra/Group/Action/Pi.lean
index 5b2184f0ed373..fee7853a61d3f 100644
--- a/Mathlib/Algebra/Group/Action/Pi.lean
+++ b/Mathlib/Algebra/Group/Action/Pi.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
 import Mathlib.Algebra.Group.Action.Faithful
+import Mathlib.Algebra.Group.Pi.Basic
 import Mathlib.Data.Set.Function
 
 /-!
diff --git a/Mathlib/Algebra/Group/Action/Pretransitive.lean b/Mathlib/Algebra/Group/Action/Pretransitive.lean
index cbbc533efdfc1..5617b5cac67aa 100644
--- a/Mathlib/Algebra/Group/Action/Pretransitive.lean
+++ b/Mathlib/Algebra/Group/Action/Pretransitive.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Action.TypeTags
+import Mathlib.Algebra.Group.Hom.Instances
 
 /-!
 # Pretransitive group actions
@@ -75,31 +76,11 @@ end MulAction
 
 namespace MulAction
 
-variable (α)
-
-/-- If an action is transitive, then composing this action with a surjective homomorphism gives
-again a transitive action. -/
-@[to_additive]
-lemma isPretransitive_compHom {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G]
-    [IsPretransitive F G] {f : E →* F} (hf : Surjective f) :
-    letI : MulAction E G := MulAction.compHom _ f
-    IsPretransitive E G := by
-  let _ : MulAction E G := MulAction.compHom _ f
-  refine ⟨fun x y ↦ ?_⟩
-  obtain ⟨m, rfl⟩ : ∃ m : F, m • x = y := exists_smul_eq F x y
-  obtain ⟨e, rfl⟩ : ∃ e, f e = m := hf m
-  exact ⟨e, rfl⟩
-
 @[to_additive]
 lemma IsPretransitive.of_smul_eq {M N α : Type*} [SMul M α] [SMul N α] [IsPretransitive M α]
     (f : M → N) (hf : ∀ {c : M} {x : α}, f c • x = c • x) : IsPretransitive N α where
   exists_smul_eq x y := (exists_smul_eq x y).elim fun m h ↦ ⟨f m, hf.trans h⟩
 
-@[to_additive]
-lemma IsPretransitive.of_compHom {M N α : Type*} [Monoid M] [Monoid N] [MulAction N α]
-    (f : M →* N) [h : letI := compHom α f; IsPretransitive M α] : IsPretransitive N α :=
-  letI := compHom α f; h.of_smul_eq f rfl
-
 end MulAction
 
 section CompatibleScalar
diff --git a/Mathlib/Algebra/Group/Action/Prod.lean b/Mathlib/Algebra/Group/Action/Prod.lean
index 898caa223cdc3..33695b40edc32 100644
--- a/Mathlib/Algebra/Group/Action/Prod.lean
+++ b/Mathlib/Algebra/Group/Action/Prod.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Eric Wieser
 -/
 import Mathlib.Algebra.Group.Action.Faithful
+import Mathlib.Algebra.Group.Action.Hom
 import Mathlib.Algebra.Group.Prod
 
 /-!
diff --git a/Mathlib/Algebra/Group/Action/TypeTags.lean b/Mathlib/Algebra/Group/Action/TypeTags.lean
index 1e65ced1a6024..c17fd1cc7e6fa 100644
--- a/Mathlib/Algebra/Group/Action/TypeTags.lean
+++ b/Mathlib/Algebra/Group/Action/TypeTags.lean
@@ -3,8 +3,9 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yury Kudryashov
 -/
-import Mathlib.Algebra.Group.Action.End
-import Mathlib.Algebra.Group.TypeTags.Hom
+import Mathlib.Algebra.Group.Action.Defs
+import Mathlib.Algebra.Group.TypeTags.Basic
+import Mathlib.Tactic.MinImports
 
 /-!
 # Additive and Multiplicative for group actions
@@ -14,7 +15,7 @@ import Mathlib.Algebra.Group.TypeTags.Hom
 group action
 -/
 
-assert_not_exists MonoidWithZero
+assert_not_exists MonoidWithZero MonoidHom
 
 open Function (Injective Surjective)
 
@@ -55,18 +56,3 @@ instance Multiplicative.smulCommClass [VAdd α γ] [VAdd β γ] [VAddCommClass 
   ⟨@vadd_comm α β _ _ _ _⟩
 
 end
-
-/-- The tautological additive action by `Additive (Function.End α)` on `α`. -/
-instance AddAction.functionEnd : AddAction (Additive (Function.End α)) α := inferInstance
-
-/-- The additive monoid hom representing an additive monoid action.
-
-When `M` is a group, see `AddAction.toPermHom`. -/
-def AddAction.toEndHom [AddMonoid M] [AddAction M α] : M →+ Additive (Function.End α) :=
-  MonoidHom.toAdditive'' MulAction.toEndHom
-
-/-- The additive action induced by a hom to `Additive (Function.End α)`
-
-See note [reducible non-instances]. -/
-abbrev AddAction.ofEndHom [AddMonoid M] (f : M →+ Additive (Function.End α)) : AddAction M α :=
-  AddAction.compHom α f
diff --git a/Mathlib/Algebra/Group/Aut.lean b/Mathlib/Algebra/Group/Aut.lean
index e4e44343e237c..dc84a1e6d2516 100644
--- a/Mathlib/Algebra/Group/Aut.lean
+++ b/Mathlib/Algebra/Group/Aut.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 -/
+import Mathlib.Algebra.Group.Action.Basic
 import Mathlib.Algebra.Group.Equiv.TypeTags
 import Mathlib.GroupTheory.Perm.Basic
 
@@ -289,3 +290,18 @@ def MulAutMultiplicative [AddGroup G] : MulAut (Multiplicative G) ≃* AddAut G
 @[simps!]
 def AddAutAdditive [Group G] : AddAut (Additive G) ≃* MulAut G :=
   { MulEquiv.toAdditive.symm with map_mul' := fun _ _ ↦ rfl }
+
+section MulDistribMulAction
+variable [Group G] [Monoid M] [MulDistribMulAction G M]
+variable (M)
+
+/-- Each element of the group defines a multiplicative monoid isomorphism.
+
+This is a stronger version of `MulAction.toPermHom`. -/
+@[simps]
+def MulDistribMulAction.toMulAut : G →* MulAut M where
+  toFun := MulDistribMulAction.toMulEquiv M
+  map_one' := MulEquiv.ext (one_smul _)
+  map_mul' _ _ := MulEquiv.ext (mul_smul _ _)
+
+end MulDistribMulAction
diff --git a/Mathlib/Algebra/GroupWithZero/Action/Basic.lean b/Mathlib/Algebra/GroupWithZero/Action/Basic.lean
index 39b682e9f1e61..9d37a3c95304d 100644
--- a/Mathlib/Algebra/GroupWithZero/Action/Basic.lean
+++ b/Mathlib/Algebra/GroupWithZero/Action/Basic.lean
@@ -98,31 +98,6 @@ def smulMonoidWithZeroHom [MonoidWithZero M₀] [MulZeroOneClass N₀] [MulActio
     [IsScalarTower M₀ N₀ N₀] [SMulCommClass M₀ N₀ N₀] : M₀ × N₀ →*₀ N₀ :=
   { smulMonoidHom with map_zero' := smul_zero _ }
 
-section MulDistribMulAction
-variable [Group G] [Monoid M] [MulDistribMulAction G M]
-variable (M)
-
-/-- Each element of the group defines a multiplicative monoid isomorphism.
-
-This is a stronger version of `MulAction.toPerm`. -/
-@[simps (config := { simpRhs := true })]
-def MulDistribMulAction.toMulEquiv (x : G) : M ≃* M :=
-  { MulDistribMulAction.toMonoidHom M x, MulAction.toPermHom G M x with }
-
-variable (G)
-
-/-- Each element of the group defines a multiplicative monoid isomorphism.
-
-This is a stronger version of `MulAction.toPermHom`. -/
-@[simps]
-def MulDistribMulAction.toMulAut : G →* MulAut M where
-  toFun := MulDistribMulAction.toMulEquiv M
-  map_one' := MulEquiv.ext (one_smul _)
-  map_mul' _ _ := MulEquiv.ext (mul_smul _ _)
-
-end MulDistribMulAction
-
-
 namespace MulAut
 
 /-- The tautological action by `MulAut M` on `M`.
diff --git a/Mathlib/Algebra/GroupWithZero/Action/Defs.lean b/Mathlib/Algebra/GroupWithZero/Action/Defs.lean
index 50cdf5c5fbf84..0e2c3920cbfff 100644
--- a/Mathlib/Algebra/GroupWithZero/Action/Defs.lean
+++ b/Mathlib/Algebra/GroupWithZero/Action/Defs.lean
@@ -257,80 +257,6 @@ theorem smul_sub (r : M) (x y : A) : r • (x - y) = r • x - r • y := by
 
 end
 
-/-- Typeclass for multiplicative actions on multiplicative structures. This generalizes
-conjugation actions. -/
-@[ext]
-class MulDistribMulAction (M : Type*) (A : Type*) [Monoid M] [Monoid A] extends
-  MulAction M A where
-  /-- Distributivity of `•` across `*` -/
-  smul_mul : ∀ (r : M) (x y : A), r • (x * y) = r • x * r • y
-  /-- Multiplying `1` by a scalar gives `1` -/
-  smul_one : ∀ r : M, r • (1 : A) = 1
-
-export MulDistribMulAction (smul_one)
-
-section
-
-variable [Monoid M] [Monoid A] [MulDistribMulAction M A]
-
-theorem smul_mul' (a : M) (b₁ b₂ : A) : a • (b₁ * b₂) = a • b₁ * a • b₂ :=
-  MulDistribMulAction.smul_mul _ _ _
-
-/-- Pullback a multiplicative distributive multiplicative action along an injective monoid
-homomorphism.
-See note [reducible non-instances]. -/
-protected abbrev Function.Injective.mulDistribMulAction [Monoid B] [SMul M B] (f : B →* A)
-    (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulDistribMulAction M B :=
-  { hf.mulAction f smul with
-    smul_mul := fun c x y => hf <| by simp only [smul, f.map_mul, smul_mul'],
-    smul_one := fun c => hf <| by simp only [smul, f.map_one, smul_one] }
-
-/-- Pushforward a multiplicative distributive multiplicative action along a surjective monoid
-homomorphism.
-See note [reducible non-instances]. -/
-protected abbrev Function.Surjective.mulDistribMulAction [Monoid B] [SMul M B] (f : A →* B)
-    (hf : Surjective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulDistribMulAction M B :=
-  { hf.mulAction f smul with
-    smul_mul := fun c x y => by
-      rcases hf x with ⟨x, rfl⟩
-      rcases hf y with ⟨y, rfl⟩
-      simp only [smul_mul', ← smul, ← f.map_mul],
-    smul_one := fun c => by rw [← f.map_one, ← smul, smul_one] }
-
-variable (A)
-
-/-- Scalar multiplication by `r` as a `MonoidHom`. -/
-def MulDistribMulAction.toMonoidHom (r : M) :
-    A →* A where
-  toFun := (r • ·)
-  map_one' := smul_one r
-  map_mul' := smul_mul' r
-
-variable {A}
-
-@[simp]
-theorem MulDistribMulAction.toMonoidHom_apply (r : M) (x : A) :
-    MulDistribMulAction.toMonoidHom A r x = r • x :=
-  rfl
-
-@[simp] lemma smul_pow' (r : M) (x : A) (n : ℕ) : r • x ^ n = (r • x) ^ n :=
-  (MulDistribMulAction.toMonoidHom _ _).map_pow _ _
-
-end
-
-section
-
-variable [Monoid M] [Group A] [MulDistribMulAction M A]
-
-@[simp]
-theorem smul_inv' (r : M) (x : A) : r • x⁻¹ = (r • x)⁻¹ :=
-  (MulDistribMulAction.toMonoidHom A r).map_inv x
-
-theorem smul_div' (r : M) (x y : A) : r • (x / y) = r • x / r • y :=
-  map_div (MulDistribMulAction.toMonoidHom A r) x y
-
-end
-
 section Group
 variable [Group α] [AddMonoid β] [DistribMulAction α β]
 
diff --git a/Mathlib/Algebra/GroupWithZero/Action/End.lean b/Mathlib/Algebra/GroupWithZero/Action/End.lean
index 35b8ca4a9efd4..a5cb38490ff74 100644
--- a/Mathlib/Algebra/GroupWithZero/Action/End.lean
+++ b/Mathlib/Algebra/GroupWithZero/Action/End.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yury Kudryashov
 -/
-import Mathlib.Algebra.Group.Action.End
+import Mathlib.Algebra.Group.Action.Hom
 import Mathlib.Algebra.Group.Equiv.Defs
 import Mathlib.Algebra.GroupWithZero.Action.Defs
 import Mathlib.Algebra.GroupWithZero.Action.Units
diff --git a/Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean b/Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
index 0de5a19d7fbc0..62c440d094045 100644
--- a/Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
+++ b/Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
@@ -190,7 +190,7 @@ open scoped RightActions
       MulOpposite.op_inv, inv_eq_zero, MulOpposite.op_eq_zero_iff, inv_inv,
       MulOpposite.smul_eq_mul_unop, MulOpposite.unop_op, mul_inv_rev, ha]
 
-@[simp] lemma inv_op_smul_finset_distrib₀ (a : α) (s : Finset α) : (s <• a)⁻¹ = a⁻¹ • s⁻¹ := by
+lemma inv_op_smul_finset_distrib₀ (a : α) (s : Finset α) : (s <• a)⁻¹ = a⁻¹ • s⁻¹ := by
   obtain rfl | ha := eq_or_ne a 0
   · obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]
   -- was `simp` and very slow (https://github.com/leanprover-community/mathlib4/issues/19751)
diff --git a/Mathlib/Algebra/Module/Defs.lean b/Mathlib/Algebra/Module/Defs.lean
index d238d1b4ce8a1..2ff05eb83726d 100644
--- a/Mathlib/Algebra/Module/Defs.lean
+++ b/Mathlib/Algebra/Module/Defs.lean
@@ -3,7 +3,6 @@ Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
-import Mathlib.Algebra.Group.Action.End
 import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Algebra.GroupWithZero.Action.Defs
 import Mathlib.Algebra.Ring.Defs
diff --git a/Mathlib/Algebra/Module/LocalizedModule/Basic.lean b/Mathlib/Algebra/Module/LocalizedModule/Basic.lean
index da3205170222f..75fe610a07e66 100644
--- a/Mathlib/Algebra/Module/LocalizedModule/Basic.lean
+++ b/Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@@ -235,8 +235,8 @@ instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} :
           on_goal 1 => rw [e₁, e₂]
           on_goal 2 => rw [eq_comm]
           all_goals
-            rw [smul_smul, mul_mul_mul_comm, ← smul_eq_mul, ← smul_eq_mul A, smul_smul_smul_comm,
-              mul_smul, mul_smul])
+            rw [smul_smul, mul_mul_mul_comm, ← smul_eq_mul, ← smul_eq_mul (α := A),
+              smul_smul_smul_comm, mul_smul, mul_smul])
     one := mk 1 (1 : S)
     one_mul := by
       rintro ⟨a, s⟩
diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
index c496fa978f0bb..ad730c2335b3f 100644
--- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
+++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
@@ -532,7 +532,7 @@ lemma image_basicOpen_eq_basicOpen (a : A) (i : ℕ) :
     (PrimeSpectrum.basicOpen (R := A⁰_ f) <|
       HomogeneousLocalization.mk
         ⟨m * i, ⟨decompose 𝒜 a i ^ m,
-          (smul_eq_mul ℕ) ▸ SetLike.pow_mem_graded _ (Submodule.coe_mem _)⟩,
+          smul_eq_mul m i ▸ SetLike.pow_mem_graded _ (Submodule.coe_mem _)⟩,
           ⟨f^i, by rw [mul_comm]; exact SetLike.pow_mem_graded _ f_deg⟩, ⟨i, rfl⟩⟩).1 :=
   Set.preimage_injective.mpr (toSpec_surjective 𝒜 f_deg hm) <|
     Set.preimage_image_eq _ (toSpec_injective 𝒜 f_deg hm) ▸ by
diff --git a/Mathlib/GroupTheory/GroupAction/Defs.lean b/Mathlib/GroupTheory/GroupAction/Defs.lean
index fe04a1f0932df..d137c682f406a 100644
--- a/Mathlib/GroupTheory/GroupAction/Defs.lean
+++ b/Mathlib/GroupTheory/GroupAction/Defs.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
+import Mathlib.Algebra.Group.Action.Basic
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
 import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.GroupWithZero.Action.Defs
@@ -22,7 +23,6 @@ This file defines orbits, stabilizers, and other objects defined in terms of act
 
 -/
 
-
 universe u v
 
 open Pointwise
@@ -180,6 +180,7 @@ lemma FixedPoints.mem_submonoid (a : α) : a ∈ submonoid M α ↔ ∀ m : M, m
 
 end Monoid
 
+-- TODO: The following two sections
 section Group
 namespace FixedPoints
 variable [Group α] [MulDistribMulAction M α]
@@ -203,6 +204,7 @@ lemma subgroup_toSubmonoid : (α^*M).toSubmonoid = submonoid M α :=
 end FixedPoints
 end Group
 
+-- TODO: The following two sections are about ring-like structures. They should move to a later file
 section AddMonoid
 
 variable [AddMonoid α] [DistribMulAction M α]
diff --git a/Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean b/Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean
index 41659e7b7b8be..1b35f76403b0e 100644
--- a/Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean
+++ b/Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean
@@ -3,9 +3,8 @@ Copyright (c) 2023 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.Group.Opposite
+import Mathlib.Algebra.Group.Action.Basic
 import Mathlib.Algebra.Group.Pi.Lemmas
-import Mathlib.Algebra.Group.Action.Faithful
 import Mathlib.Algebra.GroupWithZero.Action.Defs
 import Mathlib.Algebra.Ring.Defs
 
diff --git a/Mathlib/GroupTheory/GroupAction/Hom.lean b/Mathlib/GroupTheory/GroupAction/Hom.lean
index 941d1d43913dc..a01208e7040a1 100644
--- a/Mathlib/GroupTheory/GroupAction/Hom.lean
+++ b/Mathlib/GroupTheory/GroupAction/Hom.lean
@@ -576,8 +576,7 @@ variable {σ : R →* S}
 @[ext]
 theorem ext_ring {f g : R →ₑ+[σ] N'} (h : f 1 = g 1) : f = g := by
   ext x
-  rw [← mul_one x, ← smul_eq_mul R, f.map_smulₑ, g.map_smulₑ, h]
-
+  rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]
 
 end Semiring
 
diff --git a/Mathlib/GroupTheory/Perm/Basic.lean b/Mathlib/GroupTheory/Perm/Basic.lean
index 3ab26e2457edb..1ff330707fc31 100644
--- a/Mathlib/GroupTheory/Perm/Basic.lean
+++ b/Mathlib/GroupTheory/Perm/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
+import Mathlib.Algebra.Group.Action.End
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Units.Equiv
 import Mathlib.Algebra.GroupPower.IterateHom
diff --git a/Mathlib/GroupTheory/Subgroup/Centralizer.lean b/Mathlib/GroupTheory/Subgroup/Centralizer.lean
index 56e9672b715a0..fe6d28714cb87 100644
--- a/Mathlib/GroupTheory/Subgroup/Centralizer.lean
+++ b/Mathlib/GroupTheory/Subgroup/Centralizer.lean
@@ -3,7 +3,6 @@ Copyright (c) 2020 Kexing Ying. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying
 -/
-import Mathlib.Algebra.GroupWithZero.Action.Basic
 import Mathlib.GroupTheory.Subgroup.Center
 import Mathlib.GroupTheory.Submonoid.Centralizer
 
@@ -112,8 +111,7 @@ instance : MulDistribMulAction H.normalizer H where
 
 /-- The homomorphism N(H) → Aut(H) with kernel C(H). -/
 @[simps!]
-def normalizerMonoidHom : H.normalizer →* MulAut H :=
-  MulDistribMulAction.toMulAut H.normalizer H
+def normalizerMonoidHom : H.normalizer →* MulAut H := MulDistribMulAction.toMulAut ..
 
 theorem normalizerMonoidHom_ker :
     H.normalizerMonoidHom.ker = (Subgroup.centralizer H).subgroupOf H.normalizer := by
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
index 22f87694b197f..26a4611f0cdb7 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
@@ -353,7 +353,7 @@ open DualNumber TrivSqZeroExt
 variable {R : Type*} [CommRing R]
 
 theorem ι_mul_ι (r₁ r₂) : ι (0 : QuadraticForm R R) r₁ * ι (0 : QuadraticForm R R) r₂ = 0 := by
-  rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul R, ← smul_eq_mul R, LinearMap.map_smul,
+  rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, LinearMap.map_smul,
     LinearMap.map_smul, smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, RingHom.map_zero,
     smul_zero]
 
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
index 46fb92fde6ff3..2e4ba75fcf59b 100644
--- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
+++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
@@ -613,7 +613,7 @@ def linMulLin (f g : M →ₗ[R] A) : QuadraticMap R M A where
   toFun := f * g
   toFun_smul a x := by
     rw [Pi.mul_apply, Pi.mul_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, LinearMap.map_smulₛₗ,
-      RingHom.id_apply, smul_mul_assoc, mul_smul_comm, ← smul_assoc, (smul_eq_mul R)]
+      RingHom.id_apply, smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
   exists_companion' :=
     ⟨(LinearMap.mul R A).compl₁₂ f g + (LinearMap.mul R A).flip.compl₁₂ g f, fun x y => by
       simp only [Pi.mul_apply, map_add, left_distrib, right_distrib, LinearMap.add_apply,
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
index 0c8559a3153a9..d83c12ef1ca30 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
@@ -176,7 +176,7 @@ lemma quotTensorEquivQuotSMul_mk_tmul (I : Ideal R) (r : R) (x : M) :
   (quotTensorEquivQuotSMul M I).eq_symm_apply.mp <|
     Eq.trans (congrArg (· ⊗ₜ[R] x) <|
         Eq.trans (congrArg (Ideal.Quotient.mk I)
-                    (Eq.trans (smul_eq_mul R) (mul_one r))).symm <|
+                    (Eq.trans (smul_eq_mul ..) (mul_one r))).symm <|
           Submodule.Quotient.mk_smul I r 1) <|
       smul_tmul r _ x
 
diff --git a/Mathlib/MeasureTheory/Integral/Asymptotics.lean b/Mathlib/MeasureTheory/Integral/Asymptotics.lean
index 4ec76c13473b6..4a96e94c507ec 100644
--- a/Mathlib/MeasureTheory/Integral/Asymptotics.lean
+++ b/Mathlib/MeasureTheory/Integral/Asymptotics.lean
@@ -88,7 +88,7 @@ theorem IsBigO.set_integral_isBigO
   obtain ⟨t, htl, ht⟩ := hC.exists_mem
   obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
   refine isBigO_iff.mpr ⟨C * (μ s).toReal, eventually_iff_exists_mem.mpr ⟨v, hv, fun x hx ↦ ?_⟩⟩
-  rw [mul_assoc, ← smul_eq_mul (a' := ‖g x‖), ← MeasureTheory.Measure.restrict_apply_univ,
+  rw [mul_assoc, ← smul_eq_mul _ ‖g x‖, ← MeasureTheory.Measure.restrict_apply_univ,
     ← integral_const, mul_comm, ← smul_eq_mul, ← integral_smul_const]
   haveI : IsFiniteMeasure (μ.restrict s) := ⟨by rw [Measure.restrict_apply_univ s]; exact hμ⟩
   refine (norm_integral_le_integral_norm _).trans <|
diff --git a/Mathlib/MeasureTheory/Integral/SetIntegral.lean b/Mathlib/MeasureTheory/Integral/SetIntegral.lean
index fe4b888207acb..3985d9c8c7f1c 100644
--- a/Mathlib/MeasureTheory/Integral/SetIntegral.lean
+++ b/Mathlib/MeasureTheory/Integral/SetIntegral.lean
@@ -455,7 +455,7 @@ theorem integral_indicator_const [CompleteSpace E] (e : E) ⦃s : Set X⦄ (s_me
 @[simp]
 theorem integral_indicator_one ⦃s : Set X⦄ (hs : MeasurableSet s) :
     ∫ x, s.indicator 1 x ∂μ = (μ s).toReal :=
-  (integral_indicator_const 1 hs).trans ((smul_eq_mul _).trans (mul_one _))
+  (integral_indicator_const 1 hs).trans ((smul_eq_mul ..).trans (mul_one _))
 
 theorem setIntegral_indicatorConstLp [CompleteSpace E]
     {p : ℝ≥0∞} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμt : μ t ≠ ∞) (e : E) :
diff --git a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean
index 6365f176ee96a..b19c259133cb1 100644
--- a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean
+++ b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean
@@ -101,7 +101,7 @@ theorem unique_topology_of_t2 {t : TopologicalSpace 𝕜} (h₁ : @TopologicalAd
       -- `ξ₀ ∈ 𝓑 ⊆ {ξ₀}ᶜ`, which is a contradiction.
       by_contra! h
       suffices (ξ₀ * ξ⁻¹) • ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ by
-        rw [smul_eq_mul 𝕜, mul_assoc, inv_mul_cancel₀ hξ0, mul_one] at this
+        rw [smul_eq_mul, mul_assoc, inv_mul_cancel₀ hξ0, mul_one] at this
         exact not_mem_compl_iff.mpr (mem_singleton ξ₀) ((balancedCore_subset _) this)
       -- For that, we use that `𝓑` is balanced : since `‖ξ₀‖ < ε < ‖ξ‖`, we have `‖ξ₀ / ξ‖ ≤ 1`,
       -- hence `ξ₀ = (ξ₀ / ξ) • ξ ∈ 𝓑` because `ξ ∈ 𝓑`.