rw [he, Zsqrtd.norm_def, Zsqrtd.norm_def]
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.norm = (c + m * ↑x).norm - x * e
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)