obtain ⟨⟨c, hc⟩, ⟨d, hd⟩⟩ | ⟨hre, him⟩ := hparity
a : ℤ√(-3)
heven : Even a.norm
hparity : Even a.re ∧ Even a.im ∨ Odd a.re ∧ Odd a.im
⊢ ∃ b, a.norm = 4 * b.norm
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ ∃ b, a.norm = 4 * b.norm

case inr.intro
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
⊢ ∃ b, a.norm = 4 * b.norm