case inl
w : ℤ
h : 1 * w = -1
⊢ 1 = 1 ∧ w = -1 ∨ 1 = -1 ∧ w = 1

case inr
w : ℤ
h : -1 * w = -1
⊢ -1 = 1 ∧ w = -1 ∨ -1 = -1 ∧ w = 1
z w : ℤ
h : z * w = -1
⊢ z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
rcases isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1 with (rfl | rfl)
no goals
case inl
w : ℤ
h : 1 * w = -1
⊢ 1 = 1 ∧ w = -1 ∨ 1 = -1 ∧ w = 1
exact Or.inl ⟨rfl, one_mul w ▸ h⟩
no goals
case inr
w : ℤ
h : -1 * w = -1
⊢ -1 = 1 ∧ w = -1 ∨ -1 = -1 ∧ w = 1
exact Or.inr ⟨rfl, neg_inj.mp (neg_one_mul w ▸ h)⟩