obtain ⟨p, hpdvd, hp⟩ := OddPrimeOrFour.exists_and_dvd h2
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
case intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a