refactor(Data/Int/Units): golf isUnit_eq_or_eq_neg (#6952)

This PR adds an `IsUnit` version of `units_ne_iff_eq_neg` and uses it to golf `isUnit_eq_or_eq_neg`.

Author: tb65536

Mathlib/Data/Int/Units.lean

@@ -42,6 +42,9 @@ theorem units_ne_iff_eq_neg {u u' : ℤˣ} : u ≠ u' ↔ u = -u' := by
   rcases units_eq_one_or u' with rfl | rfl <;>
   decide
 
+theorem isUnit_ne_iff_eq_neg {u u' : ℤ} (hu : IsUnit u) (hu' : IsUnit u') : u ≠ u' ↔ u = -u' := by
+  simpa only [Ne, Units.ext_iff] using units_ne_iff_eq_neg (u := hu.unit) (u' := hu'.unit)
+
 theorem isUnit_eq_one_or {a : ℤ} : IsUnit a → a = 1 ∨ a = -1
   | ⟨_, hx⟩ => hx ▸ (units_eq_one_or _).imp (congr_arg Units.val) (congr_arg Units.val)
 #align int.is_unit_eq_one_or Int.isUnit_eq_one_or
@@ -53,10 +56,8 @@ theorem isUnit_iff {a : ℤ} : IsUnit a ↔ a = 1 ∨ a = -1 := by
   · exact isUnit_one.neg
 #align int.is_unit_iff Int.isUnit_iff
 
-theorem isUnit_eq_or_eq_neg {a b : ℤ} (ha : IsUnit a) (hb : IsUnit b) : a = b ∨ a = -b := by
-  rcases isUnit_eq_one_or hb with (rfl | rfl)
-  · exact isUnit_eq_one_or ha
-  · rwa [or_comm, neg_neg, ← isUnit_iff]
+theorem isUnit_eq_or_eq_neg {a b : ℤ} (ha : IsUnit a) (hb : IsUnit b) : a = b ∨ a = -b :=
+  or_iff_not_imp_left.mpr (isUnit_ne_iff_eq_neg ha hb).mp
 #align int.is_unit_eq_or_eq_neg Int.isUnit_eq_or_eq_neg
 
 theorem eq_one_or_neg_one_of_mul_eq_one {z w : ℤ} (h : z * w = 1) : z = 1 ∨ z = -1 :=