z w : ℤ
h : z * w = 1
h' : w * z = 1
⊢ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
z w : ℤ
h : z * w = 1
⊢ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
have h' : w * z = 1 := mul_comm z w ▸ h
no goals
z w : ℤ
h : z * w = 1
h' : w * z = 1
⊢ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
rcases eq_one_or_neg_one_of_mul_eq_one h with (rfl | rfl) <;>
    rcases eq_one_or_neg_one_of_mul_eq_one h' with (rfl | rfl) <;> tauto