simp only [hre, him, Zsqrtd.norm_neg, eq_self_iff_true, Zsqrtd.neg_im, Zsqrtd.neg_re,
  and_self_iff, neg_nonneg, Ne, not_false_iff, neg_eq_zero]
case h
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ a.norm = (-a).norm ∧ 0 ≤ (-a).re ∧ (-a).im ≠ 0
no goals