feat(algebra/{invertible + group_power/lemmas}): taking inv_of (⅟_)…

… is injective (#14011)

Besides the lemma stated in the description, I also made explicit an argument that was implicit in a different lemma and swapped the arguments of `invertible_unique` in order to get the typeclass assumptions before some non-typeclass assumptions.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/inv_of_inj)

Co-authored-by: Floris van Doorn <[fpvdoorn@gmail.com](mailto:fpvdoorn@gmail.com)>

src/algebra/group_power/lemmas.lean

@@ -41,7 +41,7 @@ instance invertible_pow (m : M) [invertible m] (n : ℕ) : invertible (m ^ n) :=
 
 lemma inv_of_pow (m : M) [invertible m] (n : ℕ) [invertible (m ^ n)] :
   ⅟(m ^ n) = ⅟m ^ n :=
-@invertible_unique M _ (m ^ n) (m ^ n) rfl ‹_› (invertible_pow m n)
+@invertible_unique M _ (m ^ n) (m ^ n) _ (invertible_pow m n) rfl
 
 lemma is_unit.pow {m : M} (n : ℕ) : is_unit m → is_unit (m ^ n) :=
 λ ⟨u, hu⟩, ⟨u ^ n, by simp *⟩

src/algebra/invertible.lean

@@ -97,8 +97,8 @@ left_inv_eq_right_inv (inv_of_mul_self _) hac
 lemma inv_of_eq_left_inv [monoid α] {a b : α} [invertible a] (hac : b * a = 1) : ⅟a = b :=
 (left_inv_eq_right_inv hac (mul_inv_of_self _)).symm
 
-lemma invertible_unique {α : Type u} [monoid α] (a b : α) (h : a = b)
-  [invertible a] [invertible b] :
+lemma invertible_unique {α : Type u} [monoid α] (a b : α) [invertible a] [invertible b]
+  (h : a = b) :
   ⅟a = ⅟b :=
 by { apply inv_of_eq_right_inv, rw [h, mul_inv_of_self], }
 
@@ -177,10 +177,14 @@ by simp only [←two_mul, mul_inv_of_self]
 instance invertible_inv_of [has_one α] [has_mul α] {a : α} [invertible a] : invertible (⅟a) :=
 ⟨ a, mul_inv_of_self a, inv_of_mul_self a ⟩
 
-@[simp] lemma inv_of_inv_of [monoid α] {a : α} [invertible a] [invertible (⅟a)] :
+@[simp] lemma inv_of_inv_of [monoid α] (a : α) [invertible a] [invertible (⅟a)] :
   ⅟(⅟a) = a :=
 inv_of_eq_right_inv (inv_of_mul_self _)
 
+@[simp] lemma inv_of_inj [monoid α] {a b : α} [invertible a] [invertible b] :
+  ⅟ a = ⅟ b ↔ a = b :=
+⟨invertible_unique _ _, invertible_unique _ _⟩
+
 /-- `⅟b * ⅟a` is the inverse of `a * b` -/
 def invertible_mul [monoid α] (a b : α) [invertible a] [invertible b] : invertible (a * b) :=
 ⟨ ⅟b * ⅟a, by simp [←mul_assoc], by simp [←mul_assoc] ⟩