obtain ⟨y, hy⟩ : x ∣ c.norm :=
  by
  set e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im with he
  convert dvd_sub hfactor (dvd_mul_right x e)
  rw [he, Zsqrtd.norm_def, Zsqrtd.norm_def]
  simp only [Zsqrtd.coe_int_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re,
    Zsqrtd.coe_int_im]
  ring
case intro.intro.intro.refine'_2
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
⊢ ∃ y, Zsqrtd.norm c = x * y ∧ Int.natAbs y < Int.natAbs x
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
⊢ ∃ y, Zsqrtd.norm c = x * y ∧ Int.natAbs y < Int.natAbs x