simp only [Zsqrtd.intCast_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re,
  Zsqrtd.intCast_im]
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ c.re * c.re - -3 * c.im * c.im =
    (c + m * ↑x).re * (c + m * ↑x).re - -3 * (c + m * ↑x).im * (c + m * ↑x).im -
      x * (m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im)
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ c.re * c.re - -3 * c.im * c.im =
    (c.re + (m.re * x + -3 * m.im * 0)) * (c.re + (m.re * x + -3 * m.im * 0)) -
        -3 * (c.im + (m.re * 0 + m.im * x)) * (c.im + (m.re * 0 + m.im * x)) -
      x * (m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im)