feat(Data/Int/Units): If z * w = 1, then z = w (#2497)

This PR adds a lemma stating that if `z * w = 1`, then `z = w`.

mathlib PR: leanprover-community/mathlib#18499



Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Mathlib/Data/Int/Units.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 
 ! This file was ported from Lean 3 source module data.int.units
-! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
+! leanprover-community/mathlib commit 641b6a82006416ec431b2987b354af9311fed4f2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -62,6 +62,11 @@ theorem eq_one_or_neg_one_of_mul_eq_one' {z w : ℤ} (h : z * w = 1) :
       rcases eq_one_or_neg_one_of_mul_eq_one h' with (rfl | rfl) <;> tauto
 #align int.eq_one_or_neg_one_of_mul_eq_one' Int.eq_one_or_neg_one_of_mul_eq_one'
 
+theorem eq_of_mul_eq_one {z w : ℤ} (h : z * w = 1) : z = w :=
+  (eq_one_or_neg_one_of_mul_eq_one' h).elim 
+    (and_imp.2 (·.trans ·.symm)) (and_imp.2 (·.trans ·.symm))
+#align int.eq_of_mul_eq_one Int.eq_of_mul_eq_one
+
 theorem mul_eq_one_iff_eq_one_or_neg_one {z w : ℤ} :
     z * w = 1 ↔ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1 := by
   refine' ⟨eq_one_or_neg_one_of_mul_eq_one', fun h => Or.elim h (fun H => _) fun H => _⟩ <;>