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