rw [abs_eq <| zero_le_one' ℤ] at hp' hq'
case intro.intro.refine'_2
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : Zsqrtd.norm p = 4
hq : p.im ≠ 0
heven : Even (Zsqrtd.norm a)
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : abs p.re = 1
hq' : abs p.im = 1
⊢ a = p * (↑p.re * u) ∨ a = star p * (↑p.re * u)
case intro.intro.refine'_2
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : Zsqrtd.norm p = 4
hq : p.im ≠ 0
heven : Even (Zsqrtd.norm a)
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : p.re = 1 ∨ p.re = -1
hq' : p.im = 1 ∨ p.im = -1
⊢ a = p * (↑p.re * u) ∨ a = star p * (↑p.re * u)