From bc1fad0bad7552fd7ba855e3ffc851d7b39b4c1f Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Thu, 22 Jun 2023 09:57:57 +0000
Subject: [PATCH] chore: forward-port mathlib#19204 (#5369)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Algebra/Invertible.lean | 72 ++++++++++++++++++++++++++++++---
 1 file changed, 67 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Algebra/Invertible.lean b/Mathlib/Algebra/Invertible.lean
index 8b44569b6cdaf..b1f7819127cd5 100644
--- a/Mathlib/Algebra/Invertible.lean
+++ b/Mathlib/Algebra/Invertible.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 
 ! This file was ported from Lean 3 source module algebra.invertible
-! leanprover-community/mathlib commit 10b4e499f43088dd3bb7b5796184ad5216648ab1
+! leanprover-community/mathlib commit 722b3b152ddd5e0cf21c0a29787c76596cb6b422
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -167,12 +167,19 @@ instance Invertible.subsingleton [Monoid α] (a : α) : Subsingleton (Invertible
     exact left_inv_eq_right_inv hba hac⟩
 #align invertible.subsingleton Invertible.subsingleton
 
+/-- If `r` is invertible and `s = r` and `si = ⅟r`, then `s` is invertible with `⅟s = si`. -/
+def Invertible.copy' [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (si : α) (hs : s = r)
+    (hsi : si = ⅟ r) : Invertible s where
+  invOf := si
+  invOf_mul_self := by rw [hs, hsi, invOf_mul_self]
+  mul_invOf_self := by rw [hs, hsi, mul_invOf_self]
+#align invertible.copy' Invertible.copy'
+
 /-- If `r` is invertible and `s = r`, then `s` is invertible. -/
+@[reducible]
 def Invertible.copy [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (hs : s = r) :
-    Invertible s where
-  invOf := ⅟ r
-  invOf_mul_self := by rw [hs, invOf_mul_self]
-  mul_invOf_self := by rw [hs, mul_invOf_self]
+    Invertible s :=
+  hr.copy' _ _ hs rfl
 #align invertible.copy Invertible.copy
 
 /-- If `a` is invertible and `a = b`, then `⅟a = ⅟b`. -/
@@ -296,6 +303,13 @@ theorem invOf_mul [Monoid α] (a b : α) [Invertible a] [Invertible b] [Invertib
   invOf_eq_right_inv (by simp [← mul_assoc])
 #align inv_of_mul invOf_mul
 
+/-- A copy of `invertibleMul` for dot notation. -/
+@[reducible]
+def Invertible.mul [Monoid α] {a b : α} (_ : Invertible a) (_ : Invertible b) :
+    Invertible (a * b) :=
+  invertibleMul _ _
+#align invertible.mul Invertible.mul
+
 theorem mul_right_inj_of_invertible [Monoid α] (c : α) [Invertible c] :
     a * c = b * c ↔ a = b :=
   ⟨fun h => by simpa using congr_arg (· * ⅟c) h, congr_arg (· * _)⟩
@@ -358,6 +372,54 @@ instance (priority := 100) Invertible.ne_zero [MulZeroOneClass α] [Nontrivial 
   ⟨nonzero_of_invertible a⟩
 #align invertible.ne_zero Invertible.ne_zero
 
+section Monoid
+
+variable [Monoid α]
+
+/-- This is the `Invertible` version of `Units.isUnit_units_mul` -/
+@[reducible]
+def invertibleOfInvertibleMul (a b : α) [Invertible a] [Invertible (a * b)] : Invertible b
+    where
+  invOf := ⅟ (a * b) * a
+  invOf_mul_self := by rw [mul_assoc, invOf_mul_self]
+  mul_invOf_self := by
+    rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
+      one_mul]
+#align invertible_of_invertible_mul invertibleOfInvertibleMul
+
+/-- This is the `Invertible` version of `Units.isUnit_mul_units` -/
+@[reducible]
+def invertibleOfMulInvertible (a b : α) [Invertible (a * b)] [Invertible b] : Invertible a
+    where
+  invOf := b * ⅟ (a * b)
+  invOf_mul_self := by
+    rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
+      one_mul]
+  mul_invOf_self := by rw [← mul_assoc, mul_invOf_self]
+#align invertible_of_mul_invertible invertibleOfMulInvertible
+
+/-- `invertibleOfInvertibleMul` and `invertibleMul` as an equivalence. -/
+@[simps]
+def Invertible.mulLeft {a : α} (_ : Invertible a) (b : α) : Invertible b ≃ Invertible (a * b)
+    where
+  toFun _ := invertibleMul a b
+  invFun _ := invertibleOfInvertibleMul a _
+  left_inv _ := Subsingleton.elim _ _
+  right_inv _ := Subsingleton.elim _ _
+#align invertible.mul_left Invertible.mulLeft
+
+/-- `invertibleOfMulInvertible` and `invertibleMul` as an equivalence. -/
+@[simps]
+def Invertible.mulRight (a : α) {b : α} (_ : Invertible b) : Invertible a ≃ Invertible (a * b)
+    where
+  toFun _ := invertibleMul a b
+  invFun _ := invertibleOfMulInvertible _ b
+  left_inv _ := Subsingleton.elim _ _
+  right_inv _ := Subsingleton.elim _ _
+#align invertible.mul_right Invertible.mulRight
+
+end Monoid
+
 section MonoidWithZero
 
 variable [MonoidWithZero α]