refactor(algebra/group/basic): Migrate add_comm_group section into co…

…mm_group section (#10565)

Currently mathlib has a rich set of lemmas connecting the addition, subtraction and negation additive commutative group operations, but a far thinner collection of results for multiplication, division and inverse multiplicative commutative group operations, despite the fact that the former can be generated easily from the latter via to_additive.

This PR refactors the additive results in the `add_comm_group` section as the equivalent multiplicative results in the `comm_group` section and then recovers the additive results via to_additive. There is a complication in that unfortunately the multiplicative forms of the names of some of the `add_comm_group` lemmas collide with existing names in `group_with_zero`. I have worked around this by appending an apostrophe to the name and then manually overriding the names generated by to_additive. In a few cases, names with `1...n` appended apostrophes already existed. In these cases I have appended `n+1` apostrophes.

Previous discussion

The `add_group` section was previously tackled in #10532.

src/algebra/group/basic.lean

@@ -482,115 +482,138 @@ lemma div_mul_comm (a b c d : G) : a / b * (c / d) = a * c / (b * d) :=
 by rw [div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_assoc,
   mul_left_cancel_iff, mul_comm, mul_assoc]
 
-end comm_group
-
-section add_comm_group
--- TODO: Generalize the contents of this section with to_additive as per
--- https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238667
-variables {G : Type u} [add_comm_group G] {a b c d : G}
+variables {a b c d : G}
 
-local attribute [simp] add_assoc add_comm add_left_comm sub_eq_add_neg
+local attribute [simp] mul_assoc mul_comm mul_left_comm div_eq_mul_inv
 
-lemma sub_add_eq_sub_sub (a b c : G) : a - (b + c) = a - b - c :=
+@[to_additive]
+lemma div_mul_eq_div_div (a b c : G) : a / (b * c) = a / b / c :=
 by simp
 
-lemma neg_add_eq_sub (a b : G) : -a + b = b - a :=
+@[to_additive]
+lemma inv_mul_eq_div (a b : G) : a⁻¹ * b = b / a :=
 by simp
 
-lemma sub_add_eq_add_sub (a b c : G) : a - b + c = a + c - b :=
+@[to_additive sub_add_eq_add_sub]
+lemma div_mul_eq_mul_div' (a b c : G) : a / b * c = a * c / b :=
 by simp
 
-lemma sub_sub (a b c : G) : a - b - c = a - (b + c) :=
+@[to_additive]
+lemma div_div (a b c : G) : a / b / c = a / (b * c) :=
 by simp
 
-lemma sub_add (a b c : G) : a - b + c = a - (b - c) :=
+@[to_additive]
+lemma div_mul (a b c : G) : a / b * c = a / (b / c) :=
 by simp
 
-@[simp] lemma add_sub_add_left_eq_sub (a b c : G) : (c + a) - (c + b) = a - b :=
+@[simp, to_additive]
+lemma mul_div_mul_left_eq_div (a b c : G) : (c * a) / (c * b) = a / b :=
 by simp
 
-lemma eq_sub_of_add_eq' (h : c + a = b) : a = b - c :=
+@[to_additive eq_sub_of_add_eq']
+lemma eq_div_of_mul_eq'' (h : c * a = b) : a = b / c :=
 by simp [h.symm]
 
-lemma eq_add_of_sub_eq' (h : a - b = c) : a = b + c :=
+@[to_additive]
+lemma eq_mul_of_div_eq' (h : a / b = c) : a = b * c :=
 by simp [h.symm]
 
-lemma add_eq_of_eq_sub' (h : b = c - a) : a + b = c :=
-begin simp [h], rw [add_comm c, add_neg_cancel_left] end
+@[to_additive]
+lemma mul_eq_of_eq_div' (h : b = c / a) : a * b = c :=
+begin simp [h], rw [mul_comm c, mul_inv_cancel_left] end
 
-lemma sub_sub_self (a b : G) : a - (a - b) = b :=
-by simpa using add_neg_cancel_left a b
+@[to_additive sub_sub_self]
+lemma div_div_self' (a b : G) : a / (a / b) = b :=
+by simpa using mul_inv_cancel_left a b
 
-lemma add_sub_comm (a b c d : G) : a + b - (c + d) = (a - c) + (b - d) :=
+@[to_additive add_sub_comm]
+lemma mul_div_comm' (a b c d : G) : a * b / (c * d) = (a / c) * (b / d) :=
 by simp
 
-lemma sub_eq_sub_add_sub (a b c : G) : a - b = c - b + (a - c) :=
-begin simp, rw [add_left_comm c], simp end
+@[to_additive]
+lemma div_eq_div_mul_div (a b c : G) : a / b = c / b * (a / c) :=
+begin simp, rw [mul_left_comm c], simp end
 
-lemma neg_neg_sub_neg (a b : G) : - (-a - -b) = a - b :=
+@[to_additive]
+lemma inv_inv_div_inv (a b : G) : (a⁻¹ / b⁻¹)⁻¹ = a / b :=
 by simp
 
-@[simp] lemma sub_sub_cancel (a b : G) : a - (a - b) = b := sub_sub_self a b
+@[simp, to_additive]
+lemma div_div_cancel (a b : G) : a / (a / b) = b := div_div_self' a b
 
-@[simp] lemma sub_sub_cancel_left (a b : G) : a - b - a = -b := by simp
+@[to_additive sub_eq_neg_add]
+lemma div_eq_inv_mul' (a b : G) : a / b = b⁻¹ * a :=
+by rw [div_eq_mul_inv, mul_comm _ _]
 
-lemma sub_eq_neg_add (a b : G) : a - b = -b + a :=
-by rw [sub_eq_add_neg, add_comm _ _]
+@[simp, to_additive]
+lemma div_div_cancel_left (a b : G) : a / b / a = b⁻¹ := by simp
 
-theorem neg_add' (a b : G) : -(a + b) = -a - b :=
-by rw [sub_eq_add_neg, neg_add a b]
+@[to_additive]
+theorem inv_mul' (a b : G) : (a * b)⁻¹ = a⁻¹ / b :=
+by rw [div_eq_mul_inv, mul_inv a b]
 
-@[simp]
-lemma neg_sub_neg (a b : G) : -a - -b = b - a :=
-by simp [sub_eq_neg_add, add_comm]
+@[simp, to_additive]
+lemma inv_div_inv (a b : G) : a⁻¹ / b⁻¹ = b / a :=
+by simp [div_eq_inv_mul', mul_comm]
 
-lemma eq_sub_iff_add_eq' : a = b - c ↔ c + a = b :=
-by rw [eq_sub_iff_add_eq, add_comm]
+@[to_additive eq_sub_iff_add_eq']
+lemma eq_div_iff_mul_eq'' : a = b / c ↔ c * a = b :=
+by rw [eq_div_iff_mul_eq', mul_comm]
 
-lemma sub_eq_iff_eq_add' : a - b = c ↔ a = b + c :=
-by rw [sub_eq_iff_eq_add, add_comm]
+@[to_additive]
+lemma div_eq_iff_eq_mul' : a / b = c ↔ a = b * c :=
+by rw [div_eq_iff_eq_mul, mul_comm]
 
-@[simp]
-lemma add_sub_cancel' (a b : G) : a + b - a = b :=
-by rw [sub_eq_neg_add, neg_add_cancel_left]
+@[simp, to_additive add_sub_cancel']
+lemma mul_div_cancel''' (a b : G) : a * b / a = b :=
+by rw [div_eq_inv_mul', inv_mul_cancel_left]
 
-@[simp]
-lemma add_sub_cancel'_right (a b : G) : a + (b - a) = b :=
-by rw [← add_sub_assoc, add_sub_cancel']
+@[simp, to_additive]
+lemma mul_div_cancel'_right (a b : G) : a * (b / a) = b :=
+by rw [← mul_div_assoc, mul_div_cancel''']
 
-@[simp] lemma sub_add_cancel' (a b : G) : a - (a + b) = -b :=
-by rw [← neg_sub, add_sub_cancel']
+@[simp, to_additive sub_add_cancel']
+lemma div_mul_cancel'' (a b : G) : a / (a * b) = b⁻¹ :=
+by rw [← inv_div', mul_div_cancel''']
 
--- This lemma is in the `simp` set under the name `add_neg_cancel_comm_assoc`,
+-- This lemma is in the `simp` set under the name `mul_inv_cancel_comm_assoc`,
+-- along with the additive version `add_neg_cancel_comm_assoc`,
 -- defined  in `algebra/group/commute`
-lemma add_add_neg_cancel'_right (a b : G) : a + (b + -a) = b :=
-by rw [← sub_eq_add_neg, add_sub_cancel'_right a b]
+@[to_additive]
+lemma mul_mul_inv_cancel'_right (a b : G) : a * (b * a⁻¹) = b :=
+by rw [← div_eq_mul_inv, mul_div_cancel'_right a b]
 
-lemma sub_right_comm (a b c : G) : a - b - c = a - c - b :=
-by { repeat { rw sub_eq_add_neg }, exact add_right_comm _ _ _ }
+@[to_additive sub_right_comm]
+lemma div_right_comm' (a b c : G) : a / b / c = a / c / b :=
+by { repeat { rw div_eq_mul_inv }, exact mul_right_comm _ _ _ }
 
-@[simp] lemma add_add_sub_cancel (a b c : G) : (a + c) + (b - c) = a + b :=
-by rw [add_assoc, add_sub_cancel'_right]
+@[simp, to_additive]
+lemma mul_mul_div_cancel (a b c : G) : (a * c) * (b / c) = a * b :=
+by rw [mul_assoc, mul_div_cancel'_right]
 
-@[simp] lemma sub_add_add_cancel (a b c : G) : (a - c) + (b + c) = a + b :=
-by rw [add_left_comm, sub_add_cancel, add_comm]
+@[simp, to_additive]
+lemma div_mul_mul_cancel (a b c : G) : (a / c) * (b * c) = a * b :=
+by rw [mul_left_comm, div_mul_cancel', mul_comm]
 
-@[simp] lemma sub_add_sub_cancel' (a b c : G) : (a - b) + (c - a) = c - b :=
-by rw add_comm; apply sub_add_sub_cancel
+@[simp, to_additive sub_add_sub_cancel']
+lemma div_mul_div_cancel'' (a b c : G) : (a / b) * (c / a) = c / b :=
+by rw mul_comm; apply div_mul_div_cancel'
 
-@[simp] lemma add_sub_sub_cancel (a b c : G) : (a + b) - (a - c) = b + c :=
-by rw [← sub_add, add_sub_cancel']
+@[simp, to_additive]
+lemma mul_div_div_cancel (a b c : G) : (a * b) / (a / c) = b * c :=
+by rw [← div_mul, mul_div_cancel''']
 
-@[simp] lemma sub_sub_sub_cancel_left (a b c : G) : (c - a) - (c - b) = b - a :=
-by rw [← neg_sub b c, sub_neg_eq_add, add_comm, sub_add_sub_cancel]
+@[simp, to_additive]
+lemma div_div_div_cancel_left (a b c : G) : (c / a) / (c / b) = b / a :=
+by rw [← inv_div' b c, div_inv_eq_mul, mul_comm, div_mul_div_cancel']
 
-lemma sub_eq_sub_iff_add_eq_add : a - b = c - d ↔ a + d = c + b :=
+@[to_additive] lemma div_eq_div_iff_mul_eq_mul : a / b = c / d ↔ a * d = c * b :=
 begin
-  rw [sub_eq_iff_eq_add, sub_add_eq_add_sub, eq_comm, sub_eq_iff_eq_add'],
-  simp only [add_comm, eq_comm]
+  rw [div_eq_iff_eq_mul, div_mul_eq_mul_div', eq_comm, div_eq_iff_eq_mul'],
+  simp only [mul_comm, eq_comm]
 end
 
-lemma sub_eq_sub_iff_sub_eq_sub : a - b = c - d ↔ a - c = b - d :=
-by rw [sub_eq_iff_eq_add, sub_add_eq_add_sub, sub_eq_iff_eq_add', add_sub_assoc]
+@[to_additive] lemma div_eq_div_iff_div_eq_div : a / b = c / d ↔ a / c = b / d :=
+by rw [div_eq_iff_eq_mul, div_mul_eq_mul_div', div_eq_iff_eq_mul', mul_div_assoc]
 
-end add_comm_group
+end comm_group