obtain ⟨c, m, rfl, h2⟩ := Zqrtd.factor_div a hodd
a : ℤ√(-3)
x : ℤ
hodd : Odd x
h : 1 < abs x
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2 ∧ c ≠ 0 ∧ ∃ y, Zsqrtd.norm c = x * y ∧ Int.natAbs y < Int.natAbs x
case intro.intro.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)
⊢ ∃ c_1 m_1,
    c + m * ↑x = c_1 + m_1 * ↑x ∧
      Zsqrtd.norm c_1 < x ^ 2 ∧ c_1 ≠ 0 ∧ ∃ y, Zsqrtd.norm c_1 = x * y ∧ Int.natAbs y < Int.natAbs x