obtain ⟨v, hv⟩ := h4
case inr.intro.inr
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re - a.im
⊢ ∃ b, a.norm = 4 * b.norm
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ ∃ b, a.norm = 4 * b.norm