chore: Rename mul-div cancellation lemmas (#11530)

Lemma names around cancellation of multiplication and division are a mess.

This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name).

| Statement           | New name                | Old name                |
|

Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

@@ -199,7 +199,7 @@ theorem exists_add_of_le : ∀ a b : L, a ≤ b → ∃ c, b = a + c := by
   · exact ⟨0, (add_zero _).symm⟩
   · exact
       ⟨⟨b - a.1, fun H => (tsub_pos_of_lt h).ne' (Prod.mk.inj_iff.1 H).1⟩,
-        Subtype.ext <| Prod.ext (add_tsub_cancel_of_le h.le).symm (add_sub_cancel'_right _ _).symm⟩
+        Subtype.ext <| Prod.ext (add_tsub_cancel_of_le h.le).symm (add_sub_cancel _ _).symm⟩
 #align counterexample.ex_L.exists_add_of_le Counterexample.ExL.exists_add_of_le
 
 theorem le_self_add : ∀ a b : L, a ≤ a + b := by

Counterexamples/HomogeneousPrimeNotPrime.lean

@@ -134,7 +134,7 @@ theorem grading.left_inv : Function.LeftInverse (coeLinearMap (grading R)) gradi
   cases' zz with a b
   unfold grading.decompose
   simp only [AddMonoidHom.coe_mk, ZeroHom.coe_mk, map_add, coeLinearMap_of, Prod.mk_add_mk,
-    add_zero, add_sub_cancel'_right]
+    add_zero, add_sub_cancel]
 #align counterexample.counterexample_not_prime_but_homogeneous_prime.grading.left_inv Counterexample.CounterexampleNotPrimeButHomogeneousPrime.grading.left_inv
 
 instance : GradedAlgebra (grading R) where

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -157,7 +157,7 @@ theorem map_ofNat_add [AddCommMonoidWithOne G] [AddMonoidWithOne H] [AddConstMap
 @[simp]
 theorem map_sub_nsmul [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b]
     (f : F) (x : G) (n : ℕ) : f (x - n • a) = f x - n • b := by
-  conv_rhs => rw [← sub_add_cancel x (n • a), map_add_nsmul, add_sub_cancel]
+  conv_rhs => rw [← sub_add_cancel x (n • a), map_add_nsmul, add_sub_cancel_right]
 
 @[simp]
 theorem map_sub_const [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b]

Mathlib/Algebra/AddTorsor.lean

@@ -64,7 +64,7 @@ instance addGroupIsAddTorsor (G : Type*) [AddGroup G] : AddTorsor G G
     where
   vsub := Sub.sub
   vsub_vadd' := sub_add_cancel
-  vadd_vsub' := add_sub_cancel
+  vadd_vsub' := add_sub_cancel_right
 #align add_group_is_add_torsor addGroupIsAddTorsor
 
 /-- Simplify subtraction for a torsor for an `AddGroup G` over
@@ -253,7 +253,7 @@ theorem vsub_sub_vsub_cancel_left (p₁ p₂ p₃ : P) : p₃ -ᵥ p₂ - (p₃
 
 @[simp]
 theorem vadd_vsub_vadd_cancel_left (v : G) (p₁ p₂ : P) : v +ᵥ p₁ -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂ := by
-  rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel']
+  rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel_left]
 #align vadd_vsub_vadd_cancel_left vadd_vsub_vadd_cancel_left
 
 theorem vsub_vadd_comm (p₁ p₂ p₃ : P) : (p₁ -ᵥ p₂ : G) +ᵥ p₃ = p₃ -ᵥ p₂ +ᵥ p₁ := by

Mathlib/Algebra/BigOperators/Basic.lean

@@ -1632,7 +1632,7 @@ theorem prod_range_div' {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
 
 @[to_additive]
 theorem eq_prod_range_div {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
-    f n = f 0 * ∏ i in range n, f (i + 1) / f i := by rw [prod_range_div, mul_div_cancel'_right]
+    f n = f 0 * ∏ i in range n, f (i + 1) / f i := by rw [prod_range_div, mul_div_cancel]
 #align finset.eq_prod_range_div Finset.eq_prod_range_div
 #align finset.eq_sum_range_sub Finset.eq_sum_range_sub
 

Mathlib/Algebra/CharZero/Lemmas.lean

@@ -168,8 +168,8 @@ section
 
 variable {R : Type*} [DivisionRing R] [CharZero R]
 
-@[simp]
-theorem half_add_self (a : R) : (a + a) / 2 = a := by rw [← mul_two, mul_div_cancel a two_ne_zero]
+@[simp] lemma half_add_self (a : R) : (a + a) / 2 = a := by
+  rw [← mul_two, mul_div_cancel_right₀ a two_ne_zero]
 #align half_add_self half_add_self
 
 @[simp]

Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean

@@ -195,12 +195,12 @@ theorem compExactValue_correctness_of_stream_eq_some :
       -- because `field_simp` is not as powerful
       have hA : (↑⌊1 / ifp_n.fr⌋ * pA + ppA) + pA * f = pA * (1 / ifp_n.fr) + ppA := by
         have := congrFun (congrArg HMul.hMul tmp_calc) f
-        rwa [right_distrib, div_mul_cancel (h := f_ne_zero),
-          div_mul_cancel (h := f_ne_zero)] at this
+        rwa [right_distrib, div_mul_cancel₀ (h := f_ne_zero),
+          div_mul_cancel₀ (h := f_ne_zero)] at this
       have hB : (↑⌊1 / ifp_n.fr⌋ * pB + ppB) + pB * f = pB * (1 / ifp_n.fr) + ppB := by
         have := congrFun (congrArg HMul.hMul tmp_calc') f
-        rwa [right_distrib, div_mul_cancel (h := f_ne_zero),
-          div_mul_cancel (h := f_ne_zero)] at this
+        rwa [right_distrib, div_mul_cancel₀ (h := f_ne_zero),
+          div_mul_cancel₀ (h := f_ne_zero)] at this
       -- now unfold the recurrence one step and simplify both sides to arrive at the conclusion
       dsimp only [conts, pconts, ppconts]
       field_simp [compExactValue, continuantsAux_recurrence s_nth_eq ppconts_eq pconts_eq,

Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean

@@ -278,7 +278,7 @@ theorem succ_nth_convergent_eq_squashGCF_nth_convergent [Field K]
       calc
         (b * g.h + a) / b = b * g.h / b + a / b := by ring
         -- requires `Field`, not `DivisionRing`
-        _ = g.h + a / b := by rw [mul_div_cancel_left _ b_ne_zero]
+        _ = g.h + a / b := by rw [mul_div_cancel_left₀ _ b_ne_zero]
     | succ n' =>
       obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.get? n' = some gp_n' :=
         g.s.ge_stable n'.le_succ s_nth_eq
@@ -323,7 +323,7 @@ theorem succ_nth_convergent_eq_squashGCF_nth_convergent [Field K]
             (continuantsAux_eq_continuantsAux_squashGCF_of_le <| le_refl <| n' + 1).symm,
             (continuantsAux_eq_continuantsAux_squashGCF_of_le n'.le_succ).symm]
         symm
-        simpa only [eq1, eq2, eq3, eq4, mul_div_cancel _ b_ne_zero]
+        simpa only [eq1, eq2, eq3, eq4, mul_div_cancel_right₀ _ b_ne_zero]
       field_simp
       congr 1 <;> ring
 #align generalized_continued_fraction.succ_nth_convergent_eq_squash_gcf_nth_convergent GeneralizedContinuedFraction.succ_nth_convergent_eq_squashGCF_nth_convergent

Mathlib/Algebra/EuclideanDomain/Defs.lean

@@ -140,7 +140,7 @@ theorem div_add_mod' (m k : R) : m / k * k + m % k = m := by
 
 theorem mod_eq_sub_mul_div {R : Type*} [EuclideanDomain R] (a b : R) : a % b = a - b * (a / b) :=
   calc
-    a % b = b * (a / b) + a % b - b * (a / b) := (add_sub_cancel' _ _).symm
+    a % b = b * (a / b) + a % b - b * (a / b) := (add_sub_cancel_left _ _).symm
     _ = a - b * (a / b) := by rw [div_add_mod]
 #align euclidean_domain.mod_eq_sub_mul_div EuclideanDomain.mod_eq_sub_mul_div
 

Mathlib/Algebra/EuclideanDomain/Instances.lean

@@ -37,7 +37,7 @@ instance (priority := 100) Field.toEuclideanDomain {K : Type*} [Field K] : Eucli
 { toCommRing := Field.toCommRing
   quotient := (· / ·), remainder := fun a b => a - a * b / b, quotient_zero := div_zero,
   quotient_mul_add_remainder_eq := fun a b => by
-    by_cases h : b = 0 <;> simp [h, mul_div_cancel']
+    by_cases h : b = 0 <;> simp [h, mul_div_cancel₀]
   r := fun a b => a = 0 ∧ b ≠ 0,
   r_wellFounded :=
     WellFounded.intro fun a =>

Mathlib/Algebra/Field/Basic.lean

@@ -55,12 +55,12 @@ theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div (ha : a ≠ 0) (hb :
 #align one_div_mul_add_mul_one_div_eq_one_div_add_one_div one_div_mul_add_mul_one_div_eq_one_div_add_one_div
 
 theorem add_div_eq_mul_add_div (a b : α) (hc : c ≠ 0) : a + b / c = (a * c + b) / c :=
-  (eq_div_iff_mul_eq hc).2 <| by rw [right_distrib, div_mul_cancel _ hc]
+  (eq_div_iff_mul_eq hc).2 <| by rw [right_distrib, div_mul_cancel₀ _ hc]
 #align add_div_eq_mul_add_div add_div_eq_mul_add_div
 
 @[field_simps]
 theorem add_div' (a b c : α) (hc : c ≠ 0) : b + a / c = (b * c + a) / c := by
-  rw [add_div, mul_div_cancel _ hc]
+  rw [add_div, mul_div_cancel_right₀ _ hc]
 #align add_div' add_div'
 
 @[field_simps]

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -988,7 +988,7 @@ theorem gcd_eq_of_dvd_sub_right {a b c : α} (h : a ∣ b - c) : gcd a b = gcd a
     rcases gcd_dvd_right a c with ⟨e, he⟩
     rcases gcd_dvd_left a c with ⟨f, hf⟩
     use e + f * d
-    rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel]
+    rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]
 #align gcd_eq_of_dvd_sub_right gcd_eq_of_dvd_sub_right
 
 theorem gcd_eq_of_dvd_sub_left {a b c : α} (h : a ∣ b - c) : gcd b a = gcd c a := by

Mathlib/Algebra/GeomSum.lean

@@ -170,7 +170,7 @@ protected theorem Commute.geom_sum₂_mul [Ring α] {x y : α} (h : Commute x y)
     (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n := by
   have := (h.sub_left (Commute.refl y)).geom_sum₂_mul_add n
   rw [sub_add_cancel] at this
-  rw [← this, add_sub_cancel]
+  rw [← this, add_sub_cancel_right]
 #align commute.geom_sum₂_mul Commute.geom_sum₂_mul
 
 theorem Commute.mul_neg_geom_sum₂ [Ring α] {x y : α} (h : Commute x y) (n : ℕ) :
@@ -266,7 +266,7 @@ theorem geom_sum₂_comm {α : Type u} [CommSemiring α] (x y : α) (n : ℕ) :
 protected theorem Commute.geom_sum₂ [DivisionRing α] {x y : α} (h' : Commute x y) (h : x ≠ y)
     (n : ℕ) : ∑ i in range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y) := by
   have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
-  rw [← h'.geom_sum₂_mul, mul_div_cancel _ this]
+  rw [← h'.geom_sum₂_mul, mul_div_cancel_right₀ _ this]
 #align commute.geom_sum₂ Commute.geom_sum₂
 
 theorem geom₂_sum [Field α] {x y : α} (h : x ≠ y) (n : ℕ) :
@@ -277,7 +277,7 @@ theorem geom₂_sum [Field α] {x y : α} (h : x ≠ y) (n : ℕ) :
 theorem geom_sum_eq [DivisionRing α] {x : α} (h : x ≠ 1) (n : ℕ) :
     ∑ i in range n, x ^ i = (x ^ n - 1) / (x - 1) := by
   have : x - 1 ≠ 0 := by simp_all [sub_eq_iff_eq_add]
-  rw [← geom_sum_mul, mul_div_cancel _ this]
+  rw [← geom_sum_mul, mul_div_cancel_right₀ _ this]
 #align geom_sum_eq geom_sum_eq
 
 protected theorem Commute.mul_geom_sum₂_Ico [Ring α] {x y : α} (h : Commute x y) {m n : ℕ}
@@ -354,7 +354,7 @@ protected theorem Commute.geom_sum₂_Ico [DivisionRing α] {x y : α} (h : Comm
     {m n : ℕ} (hmn : m ≤ n) :
     (∑ i in Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y) := by
   have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
-  rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel _ this]
+  rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel_right₀ _ this]
 #align commute.geom_sum₂_Ico Commute.geom_sum₂_Ico
 
 theorem geom_sum₂_Ico [Field α] {x y : α} (hxy : x ≠ y) {m n : ℕ} (hmn : m ≤ n) :

Mathlib/Algebra/Group/Basic.lean

@@ -804,31 +804,31 @@ theorem div_right_injective : Function.Injective fun a ↦ b / a := by
 #align div_right_injective div_right_injective
 #align sub_right_injective sub_right_injective
 
-@[to_additive (attr := simp) sub_add_cancel]
-theorem div_mul_cancel' (a b : G) : a / b * b = a :=
+@[to_additive (attr := simp)]
+theorem div_mul_cancel (a b : G) : a / b * b = a :=
   by rw [div_eq_mul_inv, inv_mul_cancel_right a b]
-#align div_mul_cancel' div_mul_cancel'
+#align div_mul_cancel' div_mul_cancel
 #align sub_add_cancel sub_add_cancel
 
 @[to_additive (attr := simp) sub_self]
 theorem div_self' (a : G) : a / a = 1 := by rw [div_eq_mul_inv, mul_right_inv a]
 #align div_self' div_self'
 #align sub_self sub_self
 
-@[to_additive (attr := simp) add_sub_cancel]
-theorem mul_div_cancel'' (a b : G) : a * b / b = a :=
+@[to_additive (attr := simp)]
+theorem mul_div_cancel_right (a b : G) : a * b / b = a :=
   by rw [div_eq_mul_inv, mul_inv_cancel_right a b]
-#align mul_div_cancel'' mul_div_cancel''
-#align add_sub_cancel add_sub_cancel
+#align mul_div_cancel'' mul_div_cancel_right
+#align add_sub_cancel add_sub_cancel_right
 
-@[to_additive (attr := simp) sub_add_cancel'']
-theorem div_mul_cancel''' (a b : G) : a / (b * a) = b⁻¹ := by rw [← inv_div, mul_div_cancel'']
-#align div_mul_cancel''' div_mul_cancel'''
-#align sub_add_cancel'' sub_add_cancel''
+@[to_additive (attr := simp)]
+lemma div_mul_cancel_right (a b : G) : a / (b * a) = b⁻¹ := by rw [← inv_div, mul_div_cancel_right]
+#align div_mul_cancel''' div_mul_cancel_right
+#align sub_add_cancel'' sub_add_cancel_right
 
 @[to_additive (attr := simp)]
 theorem mul_div_mul_right_eq_div (a b c : G) : a * c / (b * c) = a / b := by
-  rw [div_mul_eq_div_div_swap]; simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel'']
+  rw [div_mul_eq_div_div_swap]; simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel_right]
 #align mul_div_mul_right_eq_div mul_div_mul_right_eq_div
 #align add_sub_add_right_eq_sub add_sub_add_right_eq_sub
 
@@ -867,7 +867,7 @@ theorem div_left_inj : b / a = c / a ↔ b = c := by
 
 @[to_additive (attr := simp) sub_add_sub_cancel]
 theorem div_mul_div_cancel' (a b c : G) : a / b * (b / c) = a / c :=
-  by rw [← mul_div_assoc, div_mul_cancel']
+  by rw [← mul_div_assoc, div_mul_cancel]
 #align div_mul_div_cancel' div_mul_div_cancel'
 #align sub_add_sub_cancel sub_add_sub_cancel
 
@@ -918,13 +918,13 @@ theorem eq_iff_eq_of_div_eq_div (H : a / b = c / d) : a = b ↔ c = d :=
 
 @[to_additive]
 theorem leftInverse_div_mul_left (c : G) : Function.LeftInverse (fun x ↦ x / c) fun x ↦ x * c :=
-  fun x ↦ mul_div_cancel'' x c
+  fun x ↦ mul_div_cancel_right x c
 #align left_inverse_div_mul_left leftInverse_div_mul_left
 #align left_inverse_sub_add_left leftInverse_sub_add_left
 
 @[to_additive]
 theorem leftInverse_mul_left_div (c : G) : Function.LeftInverse (fun x ↦ x * c) fun x ↦ x / c :=
-  fun x ↦ div_mul_cancel' x c
+  fun x ↦ div_mul_cancel x c
 #align left_inverse_mul_left_div leftInverse_mul_left_div
 #align left_inverse_add_left_sub leftInverse_add_left_sub
 
@@ -1023,40 +1023,40 @@ theorem div_eq_iff_eq_mul' : a / b = c ↔ a = b * c := by rw [div_eq_iff_eq_mul
 #align div_eq_iff_eq_mul' div_eq_iff_eq_mul'
 #align sub_eq_iff_eq_add' sub_eq_iff_eq_add'
 
-@[to_additive (attr := simp) add_sub_cancel']
-theorem mul_div_cancel''' (a b : G) : a * b / a = b := by rw [div_eq_inv_mul, inv_mul_cancel_left]
-#align mul_div_cancel''' mul_div_cancel'''
-#align add_sub_cancel' add_sub_cancel'
+@[to_additive (attr := simp)]
+theorem mul_div_cancel_left (a b : G) : a * b / a = b := by rw [div_eq_inv_mul, inv_mul_cancel_left]
+#align mul_div_cancel''' mul_div_cancel_left
+#align add_sub_cancel' add_sub_cancel_left
 
 @[to_additive (attr := simp)]
-theorem mul_div_cancel'_right (a b : G) : a * (b / a) = b := by
-  rw [← mul_div_assoc, mul_div_cancel''']
-#align mul_div_cancel'_right mul_div_cancel'_right
-#align add_sub_cancel'_right add_sub_cancel'_right
+theorem mul_div_cancel (a b : G) : a * (b / a) = b := by
+  rw [← mul_div_assoc, mul_div_cancel_left]
+#align mul_div_cancel'_right mul_div_cancel
+#align add_sub_cancel'_right add_sub_cancel
 
-@[to_additive (attr := simp) sub_add_cancel']
-theorem div_mul_cancel'' (a b : G) : a / (a * b) = b⁻¹ := by rw [← inv_div, mul_div_cancel''']
-#align div_mul_cancel'' div_mul_cancel''
-#align sub_add_cancel' sub_add_cancel'
+@[to_additive (attr := simp)]
+theorem div_mul_cancel_left (a b : G) : a / (a * b) = b⁻¹ := by rw [← inv_div, mul_div_cancel_left]
+#align div_mul_cancel'' div_mul_cancel_left
+#align sub_add_cancel' sub_add_cancel_left
 
 -- 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`
 @[to_additive]
 theorem mul_mul_inv_cancel'_right (a b : G) : a * (b * a⁻¹) = b := by
-  rw [← div_eq_mul_inv, mul_div_cancel'_right a b]
+  rw [← div_eq_mul_inv, mul_div_cancel a b]
 #align mul_mul_inv_cancel'_right mul_mul_inv_cancel'_right
 #align add_add_neg_cancel'_right add_add_neg_cancel'_right
 
 @[to_additive (attr := simp)]
 theorem mul_mul_div_cancel (a b c : G) : a * c * (b / c) = a * b := by
-  rw [mul_assoc, mul_div_cancel'_right]
+  rw [mul_assoc, mul_div_cancel]
 #align mul_mul_div_cancel mul_mul_div_cancel
 #align add_add_sub_cancel add_add_sub_cancel
 
 @[to_additive (attr := simp)]
 theorem div_mul_mul_cancel (a b c : G) : a / c * (b * c) = a * b := by
-  rw [mul_left_comm, div_mul_cancel', mul_comm]
+  rw [mul_left_comm, div_mul_cancel, mul_comm]
 #align div_mul_mul_cancel div_mul_mul_cancel
 #align sub_add_add_cancel sub_add_add_cancel
 
@@ -1068,7 +1068,7 @@ theorem div_mul_div_cancel'' (a b c : G) : a / b * (c / a) = c / b := by
 
 @[to_additive (attr := simp)]
 theorem mul_div_div_cancel (a b c : G) : a * b / (a / c) = b * c := by
-  rw [← div_mul, mul_div_cancel''']
+  rw [← div_mul, mul_div_cancel_left]
 #align mul_div_div_cancel mul_div_div_cancel
 #align add_sub_sub_cancel add_sub_sub_cancel
 
@@ -1157,3 +1157,17 @@ set_option linter.existingAttributeWarning false in
 attribute [to_additive (attr := simp)] dite_smul smul_dite ite_smul smul_ite
 
 end ite
+
+-- 2024-03-20
+@[deprecated] alias div_mul_cancel' := div_mul_cancel
+@[deprecated] alias mul_div_cancel'' := mul_div_cancel_right
+-- The name `add_sub_cancel` was reused
+-- @[deprecated] alias add_sub_cancel := add_sub_cancel_right
+@[deprecated] alias div_mul_cancel''' := div_mul_cancel_right
+@[deprecated] alias sub_add_cancel'' := sub_add_cancel_right
+@[deprecated] alias mul_div_cancel''' := mul_div_cancel_left
+@[deprecated] alias add_sub_cancel' := add_sub_cancel_left
+@[deprecated] alias mul_div_cancel'_right := mul_div_cancel
+@[deprecated] alias add_sub_cancel'_right := add_sub_cancel
+@[deprecated] alias div_mul_cancel'' := div_mul_cancel_left
+@[deprecated] alias sub_add_cancel' := sub_add_cancel_left