fix(*): Fix errors caused by overly restrictive type-classes

src/group_theory/group_action/defs.lean

@@ -114,15 +114,6 @@ by split_ifs; refl
 
 end ite
 
-section compatible_scalar
-
-@[simp] lemma smul_one_smul {M} (N) [monoid N] [has_scalar M N] [mul_action N α] [has_scalar M α]
-  [is_scalar_tower M N α] (x : M) (y : α) :
-  (x • (1 : N)) • y = x • y :=
-by rw [smul_assoc, one_smul]
-
-end compatible_scalar
-
 namespace mul_action
 
 variables (α) [monoid α]
@@ -168,6 +159,15 @@ end mul_action
 
 end
 
+section compatible_scalar
+
+@[simp] lemma smul_one_smul {M} (N) [monoid N] [has_scalar M N] [mul_action N α] [has_scalar M α]
+  [is_scalar_tower M N α] (x : M) (y : α) :
+  (x • (1 : N)) • y = x • y :=
+by rw [smul_assoc, one_smul]
+
+end compatible_scalar
+
 /-- Typeclass for multiplicative actions on additive structures. This generalizes group modules. -/
 class distrib_mul_action (α : Type u) (β : Type v) [monoid α] [add_monoid β]
   extends mul_action α β :=