case inl
a : ℤ
ha : IsUnit a
hb : IsUnit 1
⊢ a = 1 ∨ a = -1

case inr
a : ℤ
ha : IsUnit a
hb : IsUnit (-1)
⊢ a = -1 ∨ a = - -1
a b : ℤ
ha : IsUnit a
hb : IsUnit b
⊢ a = b ∨ a = -b
rcases isUnit_eq_one_or hb with (rfl | rfl)
no goals
case inl
a : ℤ
ha : IsUnit a
hb : IsUnit 1
⊢ a = 1 ∨ a = -1
exact isUnit_eq_one_or ha
no goals
case inr
a : ℤ
ha : IsUnit a
hb : IsUnit (-1)
⊢ a = -1 ∨ a = - -1
rwa [or_comm, neg_neg, ← isUnit_iff]