chore(group_theory/group_action/defs): add instances to copy statemen…

…ts about left actions to right actions when the two are equal (#10949)

While these instances are usually available elsewhere, these shortcuts can reduce the number of typeclass assumptions other lemmas needs.
Since the instances carry no data, the only harm they can cause is performance.

There were some typeclass loops brought on by some bad instance unification, similar to the ones removed by @Vierkantor in 9ee2a50. We turn these into `lemma`s and  duplicate the docstring explaining the problem. That commit has a much longer explanation of the problem.

src/group_theory/group_action/defs.lean

@@ -195,6 +195,32 @@ mul_opposite.rec (by exact λ m, (is_central_scalar.op_smul_eq_smul _ _).symm) m
 
 export is_central_scalar (op_smul_eq_smul unop_smul_eq_smul)
 
+-- these instances are very low priority, as there is usually a faster way to find these instances
+
+@[priority 50]
+instance smul_comm_class.op_left [has_scalar M α] [has_scalar Mᵐᵒᵖ α]
+  [is_central_scalar M α] [has_scalar N α] [smul_comm_class M N α] : smul_comm_class Mᵐᵒᵖ N α :=
+⟨λ m n a, by rw [←unop_smul_eq_smul m (n • a), ←unop_smul_eq_smul m a, smul_comm]⟩
+
+@[priority 50]
+instance smul_comm_class.op_right [has_scalar M α] [has_scalar N α] [has_scalar Nᵐᵒᵖ α]
+  [is_central_scalar N α] [smul_comm_class M N α] : smul_comm_class M Nᵐᵒᵖ α :=
+⟨λ m n a, by rw [←unop_smul_eq_smul n (m • a), ←unop_smul_eq_smul n a, smul_comm]⟩
+
+@[priority 50]
+instance is_scalar_tower.op_left
+  [has_scalar M α] [has_scalar Mᵐᵒᵖ α] [is_central_scalar M α]
+  [has_scalar M N] [has_scalar Mᵐᵒᵖ N] [is_central_scalar M N]
+  [has_scalar N α] [is_scalar_tower M N α] : is_scalar_tower Mᵐᵒᵖ N α :=
+⟨λ m n a, by rw [←unop_smul_eq_smul m (n • a), ←unop_smul_eq_smul m n, smul_assoc]⟩
+
+@[priority 50]
+instance is_scalar_tower.op_right [has_scalar M α] [has_scalar M N]
+  [has_scalar N α] [has_scalar Nᵐᵒᵖ α] [is_central_scalar N α]
+  [is_scalar_tower M N α] : is_scalar_tower M Nᵐᵒᵖ α :=
+⟨λ m n a, by rw [←unop_smul_eq_smul n a, ←unop_smul_eq_smul (m • n) a, mul_opposite.unop_smul,
+                 smul_assoc]⟩
+
 namespace has_scalar
 variables [has_scalar M α]
 
@@ -230,13 +256,21 @@ lemma comp.is_scalar_tower [has_scalar M β] [has_scalar α β] [is_scalar_tower
   (by haveI := comp α g; haveI := comp β g; exact is_scalar_tower N α β) :=
 by exact {smul_assoc := λ n, @smul_assoc _ _ _ _ _ _ _ (g n) }
 
+/--
+This cannot be an instance because it can cause infinite loops whenever the `has_scalar` arguments
+are still metavariables.
+-/
 @[priority 100]
-instance comp.smul_comm_class [has_scalar β α] [smul_comm_class M β α] (g : N → M) :
+lemma comp.smul_comm_class [has_scalar β α] [smul_comm_class M β α] (g : N → M) :
   (by haveI := comp α g; exact smul_comm_class N β α) :=
 by exact {smul_comm := λ n, @smul_comm _ _ _ _ _ _ (g n) }
 
+/--
+This cannot be an instance because it can cause infinite loops whenever the `has_scalar` arguments
+are still metavariables.
+-/
 @[priority 100]
-instance comp.smul_comm_class' [has_scalar β α] [smul_comm_class β M α] (g : N → M) :
+lemma comp.smul_comm_class' [has_scalar β α] [smul_comm_class β M α] (g : N → M) :
   (by haveI := comp α g; exact smul_comm_class β N α) :=
 by exact {smul_comm := λ _ n, @smul_comm _ _ _ _ _ _ _ (g n) }