use ⟨c, d⟩
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 h
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ a.norm = 4 * { re := c, im := d }.norm