rw [this]
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
this : X.re ^ 2 = Zsqrtd.norm X - 3 * X.im ^ 2
⊢ Zsqrtd.norm p ∣ X.re ^ 2
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
this : X.re ^ 2 = Zsqrtd.norm X - 3 * X.im ^ 2
⊢ Zsqrtd.norm p ∣ Zsqrtd.norm X - 3 * X.im ^ 2