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

@@ -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. -/

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,

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) :

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 (α β)