chore: deduplicate inv_mul_cancel/mul_inv_cancel, etc. (#15717)

* `mul_left_inv`, `inv_mul_self` → `inv_mul_cancel` (for `Group`)
* `mul_right_inv`, `mul_inv_self` → `mul_inv_cancel`
* `add_left_neg`, `neg_add_self` → `neg_add_cancel` (for `AddGroup`)
* `add_right_neg`, `add_neg_self` → `add_neg_cancel`
* `inv_mul_cancel` → `inv_mul_cancel₀` (for `GroupWithZero`)
* `mul_inv_cancel` → `mul_inv_cancel₀`

Author: Parcly-Taxel

Archive/Imo/Imo2008Q3.lean

@@ -43,7 +43,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
     simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.ofNat_succ, Int.natCast_dvd_natCast.mp]
     refine (ZMod.intCast_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp ?_
     simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
-    rw [pow_two, ← hy]; exact add_left_neg 1
+    rw [pow_two, ← hy]; exact neg_add_cancel 1
   have hnat₂ : n ≤ p / 2 := ZMod.natAbs_valMinAbs_le y
   have hnat₃ : p ≥ 2 * n := by linarith [Nat.div_mul_le_self p 2]
   set k : ℕ := p - 2 * n with hnat₄

Archive/Imo/Imo2024Q2.lean

@@ -136,7 +136,7 @@ lemma ab_add_one_dvd_a_pow_large_n_add_b : a * b + 1 ∣ a ^ h.large_n + b := by
       (IsUnit.mul_right_eq_zero (ZMod.unitOfCoprime _ a_coprime_ab_add_one).isUnit).1 this
   rw [mul_add]
   norm_cast
-  simp only [mul_right_inv, Units.val_one, ZMod.coe_unitOfCoprime]
+  simp only [mul_inv_cancel, Units.val_one, ZMod.coe_unitOfCoprime]
   norm_cast
   convert ZMod.natCast_self (a * b + 1) using 2
   exact add_comm _ _

Archive/Imo/Imo2024Q6.lean

@@ -62,9 +62,9 @@ lemma Aquaesulian.apply_zero : f 0 = 0 := by
 @[simp]
 lemma Aquaesulian.apply_neg_apply_add (x : G) : f (-(f x)) + x = 0 := by
   rcases h x (-(f x)) with hc | hc
-  · rw [add_right_neg, ← h.apply_zero] at hc
+  · rw [add_neg_cancel, ← h.apply_zero] at hc
     exact h.injective hc
-  · rw [add_right_neg, h.apply_zero] at hc
+  · rw [add_neg_cancel, h.apply_zero] at hc
     exact hc.symm
 
 @[simp]

Archive/Wiedijk100Theorems/AreaOfACircle.lean

@@ -113,19 +113,19 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 := by
       ring
     · suffices -(1 : ℝ) < (r : ℝ)⁻¹ * x by exact this.ne'
       calc
-        -(1 : ℝ) = (r : ℝ)⁻¹ * -r := by simp [inv_mul_cancel hlt.ne']
+        -(1 : ℝ) = (r : ℝ)⁻¹ * -r := by simp [inv_mul_cancel₀ hlt.ne']
         _ < (r : ℝ)⁻¹ * x := by nlinarith [inv_pos.mpr hlt]
     · suffices (r : ℝ)⁻¹ * x < 1 by exact this.ne
       calc
         (r : ℝ)⁻¹ * x < (r : ℝ)⁻¹ * r := by nlinarith [inv_pos.mpr hlt]
-        _ = 1 := inv_mul_cancel hlt.ne'
+        _ = 1 := inv_mul_cancel₀ hlt.ne'
     · nlinarith
   have hcont : ContinuousOn F (Icc (-r) r) := (by continuity : Continuous F).continuousOn
   calc
     ∫ x in -r..r, 2 * f x = F r - F (-r) :=
       integral_eq_sub_of_hasDerivAt_of_le (neg_le_self r.2) hcont hderiv
         (continuous_const.mul hf).continuousOn.intervalIntegrable
     _ = NNReal.pi * (r : ℝ) ^ 2 := by
-      norm_num [F, inv_mul_cancel hlt.ne', ← mul_div_assoc, mul_comm π]
+      norm_num [F, inv_mul_cancel₀ hlt.ne', ← mul_div_assoc, mul_comm π]
 
 end Theorems100

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -285,7 +285,7 @@ lemma integral_min_eq_two_mul :
   rw [← intervalIntegral.integral_add_adjacent_intervals (b := π / 2) (c := π)]
   conv => lhs; arg 2; arg 1; intro θ; rw [← neg_neg θ, Real.sin_neg]
   · simp_rw [intervalIntegral.integral_comp_neg fun θ => min d (-θ.sin * l), ← Real.sin_add_pi,
-      intervalIntegral.integral_comp_add_right (fun θ => min d (θ.sin * l)), add_left_neg,
+      intervalIntegral.integral_comp_add_right (fun θ => min d (θ.sin * l)), neg_add_cancel,
       (by ring : -(π / 2) + π = π / 2), two_mul]
   all_goals exact intervalIntegrable_min_const_sin_mul d l _ _
 

Counterexamples/SorgenfreyLine.lean

@@ -278,7 +278,7 @@ theorem not_separatedNhds_rat_irrational_antidiag :
     `Ico x (x + k⁻¹) ×ˢ Ico (-x) (-x + k⁻¹) ⊆ V`. -/
   have : ∀ x : ℝₗ, Irrational (toReal x) →
       ∃ k : ℕ+, Ico x (x + (k : ℝₗ)⁻¹) ×ˢ Ico (-x) (-x + (k : ℝₗ)⁻¹) ⊆ V := fun x hx ↦ by
-    have hV : V ∈ 𝓝 (x, -x) := Vo.mem_nhds (@TV (x, -x) ⟨add_neg_self x, hx⟩)
+    have hV : V ∈ 𝓝 (x, -x) := Vo.mem_nhds (@TV (x, -x) ⟨add_neg_cancel x, hx⟩)
     exact (nhds_prod_antitone_basis_inv_pnat _ _).mem_iff.1 hV
   choose! k hkV using this
   /- Since the set of irrational numbers is a dense Gδ set in the usual topology of `ℝ`, there
@@ -294,7 +294,7 @@ theorem not_separatedNhds_rat_irrational_antidiag :
   /- Choose a rational number `r` in the interior of the closure of `C N`, then choose `n ≥ N > 0`
     such that `Ico r (r + n⁻¹) × Ico (-r) (-r + n⁻¹) ⊆ U`. -/
   rcases Rat.denseRange_cast.exists_mem_open isOpen_interior hN with ⟨r, hr⟩
-  have hrU : ((r, -r) : ℝₗ × ℝₗ) ∈ U := @SU (r, -r) ⟨add_neg_self _, r, rfl⟩
+  have hrU : ((r, -r) : ℝₗ × ℝₗ) ∈ U := @SU (r, -r) ⟨add_neg_cancel _, r, rfl⟩
   obtain ⟨n, hnN, hn⟩ :
       ∃ n, N ≤ n ∧ Ico (r : ℝₗ) (r + (n : ℝₗ)⁻¹) ×ˢ Ico (-r : ℝₗ) (-r + (n : ℝₗ)⁻¹) ⊆ U :=
     ((nhds_prod_antitone_basis_inv_pnat _ _).hasBasis_ge N).mem_iff.1 (Uo.mem_nhds hrU)

Mathlib/Algebra/AddTorsor.lean

@@ -146,7 +146,7 @@ theorem vadd_vsub_eq_sub_vsub (g : G) (p q : P) : g +ᵥ p -ᵥ q = g - (q -ᵥ
 as subtracting the points and subtracting that group element. -/
 theorem vsub_vadd_eq_vsub_sub (p₁ p₂ : P) (g : G) : p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g := by
   rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
-    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_self, zero_sub]
+    add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]
 
 /-- Cancellation subtracting the results of two subtractions. -/
 @[simp]

Mathlib/Algebra/Algebra/Equiv.lean

@@ -604,7 +604,7 @@ instance aut : Group (A₁ ≃ₐ[R] A₁) where
   one_mul ϕ := ext fun x => rfl
   mul_one ϕ := ext fun x => rfl
   inv := symm
-  mul_left_inv ϕ := ext <| symm_apply_apply ϕ
+  inv_mul_cancel ϕ := ext <| symm_apply_apply ϕ
 
 theorem aut_mul (ϕ ψ : A₁ ≃ₐ[R] A₁) : ϕ * ψ = ψ.trans ϕ :=
   rfl
@@ -714,8 +714,8 @@ def algHomUnitsEquiv (R S : Type*) [CommSemiring R] [Semiring S] [Algebra R S] :
   toFun := fun f ↦
     { (f : S →ₐ[R] S) with
       invFun := ↑(f⁻¹)
-      left_inv := (fun x ↦ show (↑(f⁻¹ * f) : S →ₐ[R] S) x = x by rw [inv_mul_self]; rfl)
-      right_inv := (fun x ↦ show (↑(f * f⁻¹) : S →ₐ[R] S) x = x by rw [mul_inv_self]; rfl) }
+      left_inv := (fun x ↦ show (↑(f⁻¹ * f) : S →ₐ[R] S) x = x by rw [inv_mul_cancel]; rfl)
+      right_inv := (fun x ↦ show (↑(f * f⁻¹) : S →ₐ[R] S) x = x by rw [mul_inv_cancel]; rfl) }
   invFun := fun f ↦ ⟨f, f.symm, f.comp_symm, f.symm_comp⟩
   left_inv := fun _ ↦ rfl
   right_inv := fun _ ↦ rfl

Mathlib/Algebra/BigOperators/Fin.lean

@@ -220,7 +220,7 @@ theorem partialProd_right_inv {G : Type*} [Group G] (f : Fin n → G) (i : Fin n
     simp only [partialProd_succ, mul_inv_rev, Fin.castSucc_mk]
     -- Porting note: was
     -- assoc_rw [hi, inv_mul_cancel_left]
-    rw [← mul_assoc, mul_left_eq_self, mul_assoc, hi, mul_left_inv]
+    rw [← mul_assoc, mul_left_eq_self, mul_assoc, hi, inv_mul_cancel]
 
 /-- Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
 Then if `k < j`, this says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ = gₖ`.

Mathlib/Algebra/BigOperators/Group/List.lean

@@ -435,7 +435,7 @@ lemma prod_rotate_eq_one_of_prod_eq_one :
     have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
     rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl
     rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
-      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_self, mul_one]
+      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
 
 end Group