chore: rename invOf lemmas to match inv lemmas (#16590)

This follows on from #11530

In each case, I've added an `example` with the `Group` lemma, to make it easier to keep the names in sync.

Mathlib/Algebra/Group/Invertible/Defs.lean

@@ -90,51 +90,64 @@ class Invertible [Mul α] [One α] (a : α) : Type u where
   mul_invOf_self : a * invOf = 1
 
 /-- The inverse of an `Invertible` element -/
-prefix:max
-  "⅟" =>-- This notation has the same precedence as `Inv.inv`.
-  Invertible.invOf
+-- This notation has the same precedence as `Inv.inv`.
+prefix:max "⅟" => Invertible.invOf
 
 @[simp]
 theorem invOf_mul_self' [Mul α] [One α] (a : α) {_ : Invertible a} : ⅟ a * a = 1 :=
   Invertible.invOf_mul_self
 
-theorem invOf_mul_self [Mul α] [One α] (a : α) [Invertible a] : ⅟ a * a = 1 :=
-  Invertible.invOf_mul_self
+theorem invOf_mul_self [Mul α] [One α] (a : α) [Invertible a] : ⅟ a * a = 1 := invOf_mul_self' _
 
 @[simp]
 theorem mul_invOf_self' [Mul α] [One α] (a : α) {_ : Invertible a} : a * ⅟ a = 1 :=
   Invertible.mul_invOf_self
 
-theorem mul_invOf_self [Mul α] [One α] (a : α) [Invertible a] : a * ⅟ a = 1 :=
-  Invertible.mul_invOf_self
+theorem mul_invOf_self [Mul α] [One α] (a : α) [Invertible a] : a * ⅟ a = 1 := mul_invOf_self' _
 
 @[simp]
-theorem invOf_mul_self_assoc' [Monoid α] (a b : α) {_ : Invertible a} : ⅟ a * (a * b) = b := by
+theorem invOf_mul_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : ⅟ a * (a * b) = b := by
   rw [← mul_assoc, invOf_mul_self, one_mul]
+example {G} [Group G] (a b : G) : a⁻¹ * (a * b) = b := inv_mul_cancel_left a b
 
-theorem invOf_mul_self_assoc [Monoid α] (a b : α) [Invertible a] : ⅟ a * (a * b) = b := by
-  rw [← mul_assoc, invOf_mul_self, one_mul]
+theorem invOf_mul_cancel_left [Monoid α] (a b : α) [Invertible a] : ⅟ a * (a * b) = b :=
+  invOf_mul_cancel_left' _ _
+
+@[deprecated (since := "2024-09-07")] alias invOf_mul_self_assoc' := invOf_mul_cancel_left'
+@[deprecated (since := "2024-09-07")] alias invOf_mul_self_assoc := invOf_mul_cancel_left
 
 @[simp]
-theorem mul_invOf_self_assoc' [Monoid α] (a b : α) {_ : Invertible a} : a * (⅟ a * b) = b := by
+theorem mul_invOf_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : a * (⅟ a * b) = b := by
   rw [← mul_assoc, mul_invOf_self, one_mul]
+example {G} [Group G] (a b : G) : a * (a⁻¹ * b) = b := mul_inv_cancel_left a b
 
-theorem mul_invOf_self_assoc [Monoid α] (a b : α) [Invertible a] : a * (⅟ a * b) = b := by
-  rw [← mul_assoc, mul_invOf_self, one_mul]
+theorem mul_invOf_cancel_left [Monoid α] (a b : α) [Invertible a] : a * (⅟ a * b) = b :=
+  mul_invOf_cancel_left' a b
+
+@[deprecated (since := "2024-09-07")] alias mul_invOf_self_assoc' := mul_invOf_cancel_left'
+@[deprecated (since := "2024-09-07")] alias mul_invOf_self_assoc := mul_invOf_cancel_left
 
 @[simp]
-theorem mul_invOf_mul_self_cancel' [Monoid α] (a b : α) {_ : Invertible b} : a * ⅟ b * b = a := by
+theorem invOf_mul_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * ⅟ b * b = a := by
   simp [mul_assoc]
+example {G} [Group G] (a b : G) : a * b⁻¹ * b = a := inv_mul_cancel_right a b
 
-theorem mul_invOf_mul_self_cancel [Monoid α] (a b : α) [Invertible b] : a * ⅟ b * b = a := by
-  simp [mul_assoc]
+theorem invOf_mul_cancel_right [Monoid α] (a b : α) [Invertible b] : a * ⅟ b * b = a :=
+  invOf_mul_cancel_right' _ _
+
+@[deprecated (since := "2024-09-07")] alias mul_invOf_mul_self_cancel' := invOf_mul_cancel_right'
+@[deprecated (since := "2024-09-07")] alias mul_invOf_mul_self_cancel := invOf_mul_cancel_right
 
 @[simp]
-theorem mul_mul_invOf_self_cancel' [Monoid α] (a b : α) {_ : Invertible b} : a * b * ⅟ b = a := by
+theorem mul_invOf_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * b * ⅟ b = a := by
   simp [mul_assoc]
+example {G} [Group G] (a b : G) : a * b * b⁻¹ = a := mul_inv_cancel_right a b
 
-theorem mul_mul_invOf_self_cancel [Monoid α] (a b : α) [Invertible b] : a * b * ⅟ b = a := by
-  simp [mul_assoc]
+theorem mul_invOf_cancel_right [Monoid α] (a b : α) [Invertible b] : a * b * ⅟ b = a :=
+  mul_invOf_cancel_right' _ _
+
+@[deprecated (since := "2024-09-07")] alias mul_mul_invOf_self_cancel' := mul_invOf_cancel_right'
+@[deprecated (since := "2024-09-07")] alias mul_mul_invOf_self_cancel := mul_invOf_cancel_right
 
 theorem invOf_eq_right_inv [Monoid α] {a b : α} [Invertible a] (hac : a * b = 1) : ⅟ a = b :=
   left_inv_eq_right_inv (invOf_mul_self _) hac
@@ -185,8 +198,7 @@ def invertibleOne [Monoid α] : Invertible (1 : α) :=
 theorem invOf_one' [Monoid α] {_ : Invertible (1 : α)} : ⅟ (1 : α) = 1 :=
   invOf_eq_right_inv (mul_one _)
 
-theorem invOf_one [Monoid α] [Invertible (1 : α)] : ⅟ (1 : α) = 1 :=
-  invOf_eq_right_inv (mul_one _)
+theorem invOf_one [Monoid α] [Invertible (1 : α)] : ⅟ (1 : α) = 1 := invOf_one'
 
 /-- `a` is the inverse of `⅟a`. -/
 instance invertibleInvOf [One α] [Mul α] {a : α} [Invertible a] : Invertible (⅟ a) :=
@@ -226,15 +238,15 @@ theorem mul_left_inj_of_invertible : c * a = c * b ↔ a = b :=
   ⟨fun h => by simpa using congr_arg (⅟c * ·) h, congr_arg (_ * ·)⟩
 
 theorem invOf_mul_eq_iff_eq_mul_left : ⅟c * a = b ↔ a = c * b := by
-  rw [← mul_left_inj_of_invertible (c := c), mul_invOf_self_assoc]
+  rw [← mul_left_inj_of_invertible (c := c), mul_invOf_cancel_left]
 
 theorem mul_left_eq_iff_eq_invOf_mul : c * a = b ↔ a = ⅟c * b := by
-  rw [← mul_left_inj_of_invertible (c := ⅟c), invOf_mul_self_assoc]
+  rw [← mul_left_inj_of_invertible (c := ⅟c), invOf_mul_cancel_left]
 
 theorem mul_invOf_eq_iff_eq_mul_right : a * ⅟c = b ↔ a = b * c := by
-  rw [← mul_right_inj_of_invertible (c := c), mul_invOf_mul_self_cancel]
+  rw [← mul_right_inj_of_invertible (c := c), invOf_mul_cancel_right]
 
 theorem mul_right_eq_iff_eq_mul_invOf : a * c = b ↔ a = b * ⅟c := by
-  rw [← mul_right_inj_of_invertible (c := ⅟c), mul_mul_invOf_self_cancel]
+  rw [← mul_right_inj_of_invertible (c := ⅟c), mul_invOf_cancel_right]
 
 end

Mathlib/Algebra/Symmetrized.lean

@@ -255,9 +255,9 @@ instance nonAssocSemiring [Semiring α] [Invertible (2 : α)] : NonAssocSemiring
       rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero,
         mul_zero, sym_zero]
     mul_one := fun _ => by
-      rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_self_assoc, sym_unsym]
+      rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]
     one_mul := fun _ => by
-      rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_self_assoc, sym_unsym]
+      rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]
     left_distrib := fun a b c => by
       -- Porting note: rewrote previous proof which used `match` in a way that seems unsupported.
       rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
@@ -279,10 +279,11 @@ instance [Ring α] [Invertible (2 : α)] : NonAssocRing αˢʸᵐ :=
 
 
 theorem unsym_mul_self [Semiring α] [Invertible (2 : α)] (a : αˢʸᵐ) :
-    unsym (a * a) = unsym a * unsym a := by rw [mul_def, unsym_sym, ← two_mul, invOf_mul_self_assoc]
+    unsym (a * a) = unsym a * unsym a := by
+  rw [mul_def, unsym_sym, ← two_mul, invOf_mul_cancel_left]
 
 theorem sym_mul_self [Semiring α] [Invertible (2 : α)] (a : α) : sym (a * a) = sym a * sym a := by
-  rw [sym_mul_sym, ← two_mul, invOf_mul_self_assoc]
+  rw [sym_mul_sym, ← two_mul, invOf_mul_cancel_left]
 
 theorem mul_comm [Mul α] [AddCommSemigroup α] [One α] [OfNat α 2] [Invertible (2 : α)]
     (a b : αˢʸᵐ) :

Mathlib/Data/Matrix/Invertible.lean

@@ -31,22 +31,27 @@ namespace Matrix
 section Semiring
 variable [Semiring α]
 
-/-- A copy of `invOf_mul_self_assoc` for rectangular matrices. -/
-protected theorem invOf_mul_self_assoc (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
+/-- A copy of `invOf_mul_cancel_left` for rectangular matrices. -/
+protected theorem invOf_mul_cancel_left (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
     ⅟ A * (A * B) = B := by rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_mul]
 
-/-- A copy of `mul_invOf_self_assoc` for rectangular matrices. -/
-protected theorem mul_invOf_self_assoc (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
+/-- A copy of `mul_invOf_cancel_left` for rectangular matrices. -/
+protected theorem mul_invOf_cancel_left (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
     A * (⅟ A * B) = B := by rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_mul]
 
-/-- A copy of `mul_invOf_mul_self_cancel` for rectangular matrices. -/
-protected theorem mul_invOf_mul_self_cancel (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
+/-- A copy of `invOf_mul_cancel_right` for rectangular matrices. -/
+protected theorem invOf_mul_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
     A * ⅟ B * B = A := by rw [Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one]
 
-/-- A copy of `mul_mul_invOf_self_cancel` for rectangular matrices. -/
-protected theorem mul_mul_invOf_self_cancel (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
+/-- A copy of `mul_invOf_cancel_right` for rectangular matrices. -/
+protected theorem mul_invOf_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
     A * B * ⅟ B = A := by rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]
 
+@[deprecated (since := "2024-09-07")] alias invOf_mul_self_assoc := invOf_mul_cancel_left
+@[deprecated (since := "2024-09-07")] alias mul_invOf_self_assoc := mul_invOf_cancel_left
+@[deprecated (since := "2024-09-07")] alias mul_invOf_mul_self_cancel := invOf_mul_cancel_right
+@[deprecated (since := "2024-09-07")] alias mul_mul_invOf_self_cancel := mul_invOf_cancel_right
+
 section ConjTranspose
 variable [StarRing α] (A : Matrix n n α)
 

Mathlib/LinearAlgebra/Matrix/SchurComplement.lean

@@ -53,8 +53,8 @@ theorem fromBlocks_eq_of_invertible₁₁ (A : Matrix m m α) (B : Matrix m n α
       fromBlocks 1 0 (C * ⅟ A) 1 * fromBlocks A 0 0 (D - C * ⅟ A * B) *
         fromBlocks 1 (⅟ A * B) 0 1 := by
   simp only [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, add_zero, zero_add,
-    Matrix.one_mul, Matrix.mul_one, invOf_mul_self, Matrix.mul_invOf_self_assoc,
-    Matrix.mul_invOf_mul_self_cancel, Matrix.mul_assoc, add_sub_cancel]
+    Matrix.one_mul, Matrix.mul_one, invOf_mul_self, Matrix.mul_invOf_cancel_left,
+    Matrix.invOf_mul_cancel_right, Matrix.mul_assoc, add_sub_cancel]
 
 /-- LDU decomposition of a block matrix with an invertible bottom-right corner, using the
 Schur complement. -/
@@ -78,7 +78,7 @@ def fromBlocksZero₂₁Invertible (A : Matrix m m α) (B : Matrix m n α) (D :
     [Invertible A] [Invertible D] : Invertible (fromBlocks A B 0 D) :=
   invertibleOfLeftInverse _ (fromBlocks (⅟ A) (-(⅟ A * B * ⅟ D)) 0 (⅟ D)) <| by
     simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero,
-      Matrix.neg_mul, invOf_mul_self, Matrix.mul_invOf_mul_self_cancel, add_neg_cancel,
+      Matrix.neg_mul, invOf_mul_self, Matrix.invOf_mul_cancel_right, add_neg_cancel,
       fromBlocks_one]
 
 /-- A lower-block-triangular matrix is invertible if its diagonal is. -/
@@ -88,7 +88,7 @@ def fromBlocksZero₁₂Invertible (A : Matrix m m α) (C : Matrix n m α) (D :
       (fromBlocks (⅟ A) 0 (-(⅟ D * C * ⅟ A))
         (⅟ D)) <| by -- a symmetry argument is more work than just copying the proof
     simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero,
-      Matrix.neg_mul, invOf_mul_self, Matrix.mul_invOf_mul_self_cancel, neg_add_cancel,
+      Matrix.neg_mul, invOf_mul_self, Matrix.invOf_mul_cancel_right, neg_add_cancel,
       fromBlocks_one]
 
 theorem invOf_fromBlocks_zero₂₁_eq (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α)

Mathlib/Tactic/NormNum/Basic.lean

@@ -196,11 +196,11 @@ theorem isRat_add {α} [Ring α] {f : α → α → α} {a b : α} {na nb nc : 
   have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
   have h₁ := congr_arg (↑· * (⅟↑da * ⅟↑db : α)) h₁
   simp only [Int.cast_add, Int.cast_mul, Int.cast_natCast, ← mul_assoc,
-    add_mul, mul_mul_invOf_self_cancel] at h₁
+    add_mul, mul_invOf_cancel_right] at h₁
   have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
-  simp only [H, mul_mul_invOf_self_cancel', Nat.cast_mul, ← mul_assoc] at h₁ h₂
+  simp only [H, mul_invOf_cancel_right', Nat.cast_mul, ← mul_assoc] at h₁ h₂
   rw [h₁, h₂, Nat.cast_commute]
-  simp only [mul_mul_invOf_self_cancel,
+  simp only [mul_invOf_cancel_right,
     (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
     (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]
 
@@ -382,8 +382,8 @@ theorem isRat_mul {α} [Ring α] {f : α → α → α} {a b : α} {na nb nc : 
   simp only [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, h₁]
   have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
   simp only [Nat.cast_mul, ← mul_assoc] at h₂; rw [H] at h₂
-  simp only [mul_mul_invOf_self_cancel'] at h₂; rw [h₂, Nat.cast_commute]
-  simp only [mul_mul_invOf_self_cancel,
+  simp only [mul_invOf_cancel_right'] at h₂; rw [h₂, Nat.cast_commute]
+  simp only [mul_invOf_cancel_right,
     (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
     (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]
 

Mathlib/Tactic/NormNum/Ineq.lean

@@ -62,7 +62,7 @@ theorem isRat_lt_true [LinearOrderedRing α] [Nontrivial α] : {a b : α} → {n
     have hb : 0 < ⅟(db : α) := pos_invOf_of_invertible_cast db
     have h := (mul_lt_mul_of_pos_left · hb) <| mul_lt_mul_of_pos_right h ha
     rw [← mul_assoc, Int.commute_cast] at h
-    simp? at h says simp only [Int.cast_mul, Int.cast_natCast, mul_mul_invOf_self_cancel'] at h
+    simp? at h says simp only [Int.cast_mul, Int.cast_natCast, mul_invOf_cancel_right'] at h
     rwa [Int.commute_cast] at h
 
 theorem isRat_le_false [LinearOrderedRing α] [Nontrivial α] {a b : α} {na nb : ℤ} {da db : ℕ}