simp only [iff_iff_and_or_not_and_not, ← Int.odd_iff_not_even] at hparity
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hparity : Even a.re ↔ Even a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hparity : Even a.re ∧ Even a.im ∨ Odd a.re ∧ Odd a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b