simp only [Zsqrtd.ext_iff, neg_mul, add_zero, Zsqrtd.intCast_re, MulZeroClass.zero_mul, mul_neg,
  Zsqrtd.mul_im, Zsqrtd.mul_re, neg_neg, MulZeroClass.mul_zero, neg_zero, Zsqrtd.intCast_im,
  this]
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑p.norm * U
this : p.norm = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ ↑p.norm * a =
    { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im } *
      { re := p.re, im := -↑A * p.im }
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑p.norm * U
this : p.norm = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ (p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2) * a.re =
      (p.re * a.re - ↑A * 3 * p.im * a.im) * p.re + 3 * (p.re * a.im + ↑A * a.re * p.im) * (↑A * p.im) ∧
    (p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2) * a.im =
      -((p.re * a.re - ↑A * 3 * p.im * a.im) * (↑A * p.im)) + (p.re * a.im + ↑A * a.re * p.im) * p.re