rw [Nat.abs_cast, ← Zsqrt3.norm_natAbs, Nat.cast_inj] at hcd
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
hpdvd : ↑p ∣ a.norm
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hcd : |↑p| = q'.norm
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
hpdvd : ↑p ∣ a.norm
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm