rw [Zsqrtd.norm_mul, Zsqrtd.norm_intCast, ← sq, ← sq_abs, hp', one_pow, one_mul]
case intro.intro.refine'_3
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ a.norm = 4 * (↑p.re * u).norm
case intro.intro.refine'_3
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hp : p.norm = 4
hq : p.im ≠ 0
heven : Even a.norm
u : ℤ√(-3)
q : ℤ√(-3) := { re := 1, im := 1 }
h2 : a = q * u ∨ a = star q * u
hp' : |p.re| = 1
hq' : |p.im| = 1
⊢ a.norm = 4 * u.norm