feat(*): op_op_op_comm lemmas (#13528)

A handful of lemmas of the form `op (op a b) (op c d) = op (op a c) (op b d)`.

src/algebra/group/basic.lean

@@ -507,6 +507,9 @@ by simp_rw [div_eq_mul_inv, mul_left_comm]
 lemma div_mul_div_comm (a b c d : G) : a / b * (c / d) = a * c / (b * d) :=
 by simp
 
+@[to_additive]
+lemma div_div_div_comm (a b c d : G) : (a / b) / (c / d) = (a / c) / (b / d) := by simp
+
 @[to_additive]
 lemma div_mul_eq_div_div (a b c : G) : a / (b * c) = a / b / c :=
 by simp

src/algebra/group_with_zero/basic.lean

@@ -990,6 +990,9 @@ lemma div_mul_div_comm₀ (a b c d : G₀) :
       (a / b) * (c / d) = (a * c) / (b * d) :=
 by simp [div_eq_mul_inv, mul_inv₀]
 
+lemma div_div_div_comm₀ (a b c d : G₀) : (a / b) / (c / d) = (a / c) / (b / d) :=
+by simp_rw [div_eq_mul_inv, mul_inv₀, inv_inv, mul_mul_mul_comm]
+
 lemma mul_div_mul_left (a b : G₀) {c : G₀} (hc : c ≠ 0) :
       (c * a) / (c * b) = a / b :=
 by rw [mul_comm c, mul_comm c, mul_div_mul_right _ _ hc]

src/group_theory/group_action/defs.lean

@@ -44,7 +44,7 @@ More sophisticated lemmas belong in `group_theory.group_action`.
 group action
 -/
 
-variables {M N G A B α β γ : Type*}
+variables {M N G A B α β γ δ : Type*}
 
 open function (injective surjective)
 
@@ -290,6 +290,11 @@ lemma smul_mul_assoc [has_mul β] [has_scalar α β] [is_scalar_tower α β β]
   (r • x) * y = r • (x * y) :=
 smul_assoc r x y
 
+lemma smul_smul_smul_comm [has_scalar α β] [has_scalar α γ] [has_scalar β δ] [has_scalar α δ]
+  [has_scalar γ δ] [is_scalar_tower α β δ] [is_scalar_tower α γ δ] [smul_comm_class β γ δ]
+  (a : α) (b : β) (c : γ) (d : δ) : (a • b) • (c • d) = (a • c) • b • d :=
+by { rw [smul_assoc, smul_assoc, smul_comm b], apply_instance }
+
 variables [has_scalar M α]
 
 lemma commute.smul_right [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α]

src/order/symm_diff.lean

@@ -56,7 +56,7 @@ rfl
 lemma symm_diff_eq_xor (p q : Prop) : p ∆ q = xor p q := rfl
 
 section generalized_boolean_algebra
-variables {α : Type*} [generalized_boolean_algebra α] (a b c : α)
+variables {α : Type*} [generalized_boolean_algebra α] (a b c d : α)
 
 lemma symm_diff_comm : a ∆ b = b ∆ a := by simp only [(∆), sup_comm]
 
@@ -154,6 +154,14 @@ by rw [symm_diff_symm_diff_left, symm_diff_symm_diff_right]
 
 instance symm_diff_is_assoc : is_associative α (∆) := ⟨symm_diff_assoc⟩
 
+lemma symm_diff_left_comm : a ∆ (b ∆ c) = b ∆ (a ∆ c) :=
+by simp_rw [←symm_diff_assoc, symm_diff_comm]
+
+lemma symm_diff_right_comm : a ∆ b ∆ c = a ∆ c ∆ b := by simp_rw [symm_diff_assoc, symm_diff_comm]
+
+lemma symm_diff_symm_diff_symm_diff_comm : (a ∆ b) ∆ (c ∆ d) = (a ∆ c) ∆ (b ∆ d) :=
+by simp_rw [symm_diff_assoc, symm_diff_left_comm]
+
 @[simp] lemma symm_diff_symm_diff_self : a ∆ (a ∆ b) = b := by simp [←symm_diff_assoc]
 
 @[simp] lemma symm_diff_symm_diff_self' : a ∆ b ∆ a = b :=