refine' ⟨u', _, h, h'⟩
case intro.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u' : ℤ√(-3)
h : a = p * u' ∨ a = star p * u'
h' : a.norm = p.norm * u'.norm
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
case intro.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u' : ℤ√(-3)
h : a = p * u' ∨ a = star p * u'
h' : a.norm = p.norm * u'.norm
⊢ IsCoprime u'.re u'.im