From aff6bd1b9df00a41b8590fbe38267580629de62d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 1 Mar 2021 10:35:11 +0000
Subject: [PATCH] fix(group_action/defs): make mul_action.regular an instance
 (#6241)

This is essentially already an instance via `semiring.to_semimodule.to_distrib_mul_action.to_mul_action`, but with an unecessary `semiring R` constraint.

I can't remember the details, but I've run into multiple instance resolution issues in the past that were resolved with `local attribute [instance] mul_action.regular`.

This also renames the instance to `monoid.to_mul_action` for consistency with `semiring.to_semimodule`.
---
 src/algebra/group_action_hom.lean       |  2 --
 src/algebra/module/basic.lean           |  7 +------
 src/data/finsupp/basic.lean             |  2 +-
 src/group_theory/group_action/defs.lean | 21 ++++++++++++---------
 4 files changed, 14 insertions(+), 18 deletions(-)

diff --git a/src/algebra/group_action_hom.lean b/src/algebra/group_action_hom.lean
index e4d24c8d56b6c..0a468163f8ea3 100644
--- a/src/algebra/group_action_hom.lean
+++ b/src/algebra/group_action_hom.lean
@@ -93,8 +93,6 @@ ext $ λ x, by rw [comp_apply, id_apply]
 @[simp] lemma comp_id (f : X →[M'] Y) : f.comp (mul_action_hom.id M') = f :=
 ext $ λ x, by rw [comp_apply, id_apply]
 
-local attribute [instance] mul_action.regular
-
 variables {G} (H)
 
 /-- The canonical map to the left cosets. -/
diff --git a/src/algebra/module/basic.lean b/src/algebra/module/basic.lean
index 07b767460af3a..53e867f286f70 100644
--- a/src/algebra/module/basic.lean
+++ b/src/algebra/module/basic.lean
@@ -216,16 +216,11 @@ theorem semimodule.subsingleton (R M : Type*) [semiring R] [subsingleton R] [add
 
 @[priority 910] -- see Note [lower instance priority]
 instance semiring.to_semimodule [semiring R] : semimodule R R :=
-{ smul := (*),
-  smul_add := mul_add,
+{ smul_add := mul_add,
   add_smul := add_mul,
-  mul_smul := mul_assoc,
-  one_smul := one_mul,
   zero_smul := zero_mul,
   smul_zero := mul_zero }
 
-@[simp] lemma smul_eq_mul [semiring R] {a a' : R} : a • a' = a * a' := rfl
-
 /-- A ring homomorphism `f : R →+* M` defines a module structure by `r • x = f r * x`. -/
 def ring_hom.to_semimodule [semiring R] [semiring S] (f : R →+* S) : semimodule R S :=
 { smul := λ r x, f r * x,
diff --git a/src/data/finsupp/basic.lean b/src/data/finsupp/basic.lean
index bf5f39a80e53a..a55875a1e3bb8 100644
--- a/src/data/finsupp/basic.lean
+++ b/src/data/finsupp/basic.lean
@@ -1640,7 +1640,7 @@ Scalar multiplication by a group element on finitely supported functions on a gr
 given by precomposition with the action of g⁻¹. -/
 def comap_distrib_mul_action_self :
   distrib_mul_action G (G →₀ M) :=
-@finsupp.comap_distrib_mul_action G M G _ (mul_action.regular G) _
+@finsupp.comap_distrib_mul_action G M G _ (monoid.to_mul_action G) _
 
 @[simp]
 lemma comap_smul_single (g : G) (a : α) (b : M) :
diff --git a/src/group_theory/group_action/defs.lean b/src/group_theory/group_action/defs.lean
index 919f5becf0d84..1bb5eed8894f1 100644
--- a/src/group_theory/group_action/defs.lean
+++ b/src/group_theory/group_action/defs.lean
@@ -132,24 +132,27 @@ by split_ifs; refl
 
 end ite
 
-namespace mul_action
+section
 
 variables (α)
 
-/-- The regular action of a monoid on itself by left multiplication. -/
-def regular : mul_action α α :=
-{ smul := λ a₁ a₂, a₁ * a₂,
-  one_smul := λ a, one_mul a,
-  mul_smul := λ a₁ a₂ a₃, mul_assoc _ _ _, }
+/-- The regular action of a monoid on itself by left multiplication.
 
-section regular
+This is promoted to a semimodule by `semiring.to_semimodule`. -/
+@[priority 910] -- see Note [lower instance priority]
+instance monoid.to_mul_action : mul_action α α :=
+{ smul := (*),
+  one_smul := one_mul,
+  mul_smul := mul_assoc }
 
-local attribute [instance] regular
+@[simp] lemma smul_eq_mul {a a' : α} : a • a' = a * a' := rfl
 
 instance is_scalar_tower.left : is_scalar_tower α α β :=
 ⟨λ x y z, mul_smul x y z⟩
 
-end regular
+end
+
+namespace mul_action
 
 variables (α β)