obtain ⟨ha, hb⟩ := step1a hcoprime heven
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u