refactor(group_theory/group_action/defs): generalize smul_mul_assoc and mul_smul_comm (#7441)

These lemmas did not need a full algebra structure; written this way, it permits usage on `has_scalar (units R) A` given `algebra R A` (in some future PR).

For now, the old algebra lemmas are left behind, to minimize the scope of this patch.

Author: eric-wieser

src/algebra/algebra/basic.lean

@@ -167,17 +167,22 @@ algebra.commutes' r x
 theorem left_comm (r : R) (x y : A) : x * (algebra_map R A r * y) = algebra_map R A r * (x * y) :=
 by rw [← mul_assoc, ← commutes, mul_assoc]
 
-@[simp] lemma mul_smul_comm (s : R) (x y : A) :
+instance _root_.is_scalar_tower.right : is_scalar_tower R A A :=
+⟨λ x y z, by rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]⟩
+
+/-- This is just a special case of the global `mul_smul_comm` lemma that requires less typeclass
+search (and was here first). -/
+@[simp] protected lemma mul_smul_comm (s : R) (x y : A) :
   x * (s • y) = s • (x * y) :=
+-- TODO: set up `is_scalar_tower.smul_comm_class` earlier so that we can actually prove this using
+-- `mul_smul_comm s x y`.
 by rw [smul_def, smul_def, left_comm]
 
-@[simp] lemma smul_mul_assoc (r : R) (x y : A) :
+/-- This is just a special case of the global `smul_mul_assoc` lemma that requires less typeclass
+search (and was here first). -/
+@[simp] protected lemma smul_mul_assoc (r : R) (x y : A) :
   (r • x) * y = r • (x * y) :=
-by rw [smul_def, smul_def, mul_assoc]
-
-lemma smul_mul_smul (r s : R) (x y : A) :
-  (r • x) * (s • y) = (r * s) • (x * y) :=
-by rw [algebra.smul_mul_assoc, algebra.mul_smul_comm, smul_smul]
+smul_mul_assoc r x y
 
 section
 variables {r : R} {a : A}

src/algebra/algebra/tower.lean

@@ -132,9 +132,6 @@ rfl
 
 variables (R) {S A B}
 
-instance right : is_scalar_tower S A A :=
-⟨λ x y z, by rw [smul_eq_mul, smul_eq_mul, algebra.smul_mul_assoc]⟩
-
 instance comap {R S A : Type*} [comm_semiring R] [comm_semiring S] [semiring A]
   [algebra R S] [algebra S A] : is_scalar_tower R S (algebra.comap R S A) :=
 of_algebra_map_eq $ λ x, rfl

src/group_theory/group_action/defs.lean

@@ -185,6 +185,27 @@ add_decl_doc add_monoid.to_add_action
 instance is_scalar_tower.left : is_scalar_tower M M α :=
 ⟨λ x y z, mul_smul x y z⟩
 
+variables {M}
+
+/-- Note that the `smul_comm_class M α α` typeclass argument is usually satisfied by `algebra M α`.
+-/
+@[to_additive]
+lemma mul_smul_comm [monoid α] (s : M) (x y : α) [smul_comm_class M α α] :
+  x * (s • y) = s • (x * y) :=
+(smul_comm s x y).symm
+
+/-- Note that the `is_scalar_tower M α α` typeclass argument is usually satisfied by `algebra M α`.
+-/
+lemma smul_mul_assoc [monoid α] (r : M) (x y : α) [is_scalar_tower M α α] :
+  (r • x) * y = r • (x * y) :=
+smul_assoc r x y
+
+/-- Note that the `is_scalar_tower M α α` and `smul_comm_class M α α` typeclass arguments are
+usually satisfied by `algebra M α`. -/
+lemma smul_mul_smul [monoid α] (r s : M) (x y : α) [is_scalar_tower M α α] [smul_comm_class M α α] :
+  (r • x) * (s • y) = (r * s) • (x * y) :=
+by rw [smul_mul_assoc, mul_smul_comm, smul_smul]
+
 end
 
 namespace mul_action