a : ℤ
h : a = 1 ∨ a = -1
⊢ IsUnit a
a : ℤ
⊢ IsUnit a ↔ a = 1 ∨ a = -1
refine' ⟨fun h => isUnit_eq_one_or h, fun h => _⟩
case inl

⊢ IsUnit 1

case inr

⊢ IsUnit (-1)
a : ℤ
h : a = 1 ∨ a = -1
⊢ IsUnit a
rcases h with (rfl | rfl)
no goals
case inl

⊢ IsUnit 1
exact isUnit_one
no goals
case inr

⊢ IsUnit (-1)
exact isUnit_one.neg