rw [hcd] at hpdvd hp
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
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : ↑q'.norm.natAbs ∣ a.norm
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