simp only [hp', one_mul, Zsqrtd.norm_neg, Int.cast_one, Int.cast_neg, neg_one_mul]
case intro.intro.refine'_2.inr
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
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
h4 : p = -q ∨ p = -star q
⊢ a = p * (↑p.re * u) ∨ a = star p * (↑p.re * u)
case intro.intro.refine'_2.inr
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
hq' : p.im = 1 ∨ p.im = -1
hp' : p.re = -1
h4 : p = -q ∨ p = -star q
⊢ a = p * -u ∨ a = star p * -u