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                |
|

Author: YaelDillies

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 =>