rw [Zsqrtd.norm]
case h.e'_3.h.e'_6
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ P.norm = p ^ 2 + 3 * q ^ 2
case h.e'_3.h.e'_6
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ P.re * P.re - -3 * P.im * P.im = p ^ 2 + 3 * q ^ 2