Theorem: Spts.mul_of_dvd' (FltRegular/FltThree/Spts.lean)

State before:
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
⊢ ∃ u, a = p * u ∨ a = star p * u
Tactic:
obtain ⟨f, hf⟩ := hdvd
State after:
case intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ ∃ u, a = p * u ∨ a = star p * u

State before:
case intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
⊢ ∃ u, a = p * u ∨ a = star p * u
Tactic:
obtain ⟨A, HA⟩ : ∃ A : Units ℤ, p.norm ∣ p.re * a.im + A * a.re * p.im :=
  by
  cases' h0 with h0 h0 <;> [(use -1); (use 1)] <;> convert h0 using 1 <;>
    simp only [Units.val_neg, Units.val_one, neg_mul, one_mul]
  ring
State after:
case intro.intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ p.re * a.im + ↑A * a.re * p.im
⊢ ∃ u, a = p * u ∨ a = star p * u

State before:
case intro.intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ p.re * a.im + ↑A * a.re * p.im
⊢ ∃ u, a = p * u ∨ a = star p * u
Tactic:
have HAsq : (A : ℤ) ^ 2 = 1 := by
  calc
    (A : ℤ) ^ 2 = ((A ^ 2 : Units ℤ) : ℤ) := (Units.val_pow_eq_pow_val _ _).symm
    _ = ((1 : Units ℤ) : ℤ) := (congr_arg _ (Int.units_sq A))
    _ = 1 := Units.val_one
State after:
case intro.intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
⊢ ∃ u, a = p * u ∨ a = star p * u

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
Tactic:
apply hpprime.dvd_or_dvd
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ p.norm ∣ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im)

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ p.norm ∣ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im)
Tactic:
convert dvd_mul_right p.norm (a.im ^ 2 - p.im ^ 2 * f) using 1
State after:
case h.e'_4
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) = p.norm * (a.im ^ 2 - p.im ^ 2 * f)

State before:
case h.e'_4
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) = p.norm * (a.im ^ 2 - p.im ^ 2 * f)
Tactic:
trans a.im ^ 2 * p.norm - p.im ^ 2 * (p.norm * f)
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) = a.im ^ 2 * p.norm - p.im ^ 2 * (p.norm * f)

a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ a.im ^ 2 * p.norm - p.im ^ 2 * (p.norm * f) = p.norm * (a.im ^ 2 - p.im ^ 2 * f)

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) = a.im ^ 2 * p.norm - p.im ^ 2 * (p.norm * f)
Tactic:
rw [← hf, Zsqrtd.norm_def, Zsqrtd.norm_def]
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) =
    a.im ^ 2 * (p.re * p.re - -3 * p.im * p.im) - p.im ^ 2 * (a.re * a.re - -3 * a.im * a.im)

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) =
    a.im ^ 2 * (p.re * p.re - -3 * p.im * p.im) - p.im ^ 2 * (a.re * a.re - -3 * a.im * a.im)
Tactic:
ring
State after:
no goals

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ a.im ^ 2 * p.norm - p.im ^ 2 * (p.norm * f) = p.norm * (a.im ^ 2 - p.im ^ 2 * f)
Tactic:
rw [Zsqrtd.norm_def]
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ a.im ^ 2 * (p.re * p.re - -3 * p.im * p.im) - p.im ^ 2 * ((p.re * p.re - -3 * p.im * p.im) * f) =
    (p.re * p.re - -3 * p.im * p.im) * (a.im ^ 2 - p.im ^ 2 * f)

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ a.im ^ 2 * (p.re * p.re - -3 * p.im * p.im) - p.im ^ 2 * ((p.re * p.re - -3 * p.im * p.im) * f) =
    (p.re * p.re - -3 * p.im * p.im) * (a.im ^ 2 - p.im ^ 2 * f)
Tactic:
ring
State after:
no goals

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
⊢ ∃ A, p.norm ∣ p.re * a.im + ↑A * a.re * p.im
Tactic:
cases' h0 with h0 h0 <;> [(use -1); (use 1)] <;> convert h0 using 1 <;>
  simp only [Units.val_neg, Units.val_one, neg_mul, one_mul]
State after:
case h.e'_4
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im
⊢ p.re * a.im + -(a.re * p.im) = p.re * a.im - a.re * p.im

State before:
case h.e'_4
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im
⊢ p.re * a.im + -(a.re * p.im) = p.re * a.im - a.re * p.im
Tactic:
ring
State after:
no goals

State before:
case inl
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im
⊢ ∃ A, p.norm ∣ p.re * a.im + ↑A * a.re * p.im
Tactic:
use -1
State after:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im
⊢ p.norm ∣ p.re * a.im + ↑(-1) * a.re * p.im

State before:
case inr
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im + a.re * p.im
⊢ ∃ A, p.norm ∣ p.re * a.im + ↑A * a.re * p.im
Tactic:
use 1
State after:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im + a.re * p.im
⊢ p.norm ∣ p.re * a.im + ↑1 * a.re * p.im

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ p.re * a.im + ↑A * a.re * p.im
⊢ ↑A ^ 2 = 1
Tactic:
calc
  (A : ℤ) ^ 2 = ((A ^ 2 : Units ℤ) : ℤ) := (Units.val_pow_eq_pow_val _ _).symm
  _ = ((1 : Units ℤ) : ℤ) := (congr_arg _ (Int.units_sq A))
  _ = 1 := Units.val_one
State after:
no goals

State before:
case intro.intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
⊢ ∃ u, a = p * u ∨ a = star p * u
Tactic:
set X : ℤ√(-3) := ⟨p.re * a.re - A * 3 * p.im * a.im, p.re * a.im + A * a.re * p.im⟩ with HX
State after:
case intro.intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ ∃ u, a = p * u ∨ a = star p * u

State before:
case intro.intro.intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ ∃ u, a = p * u ∨ a = star p * u
Tactic:
use U
State after:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ a = p * U ∨ a = star p * U

State before:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ a = p * U ∨ a = star p * U
Tactic:
suffices a = ⟨p.re, -A * p.im⟩ * U by
  apply Or.imp _ _ (Int.units_eq_one_or A).symm <;> rintro rfl <;> simpa [Zsqrtd.ext] using this
State after:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ a = { re := p.re, im := -↑A * p.im } * U

State before:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ a = { re := p.re, im := -↑A * p.im } * U
Tactic:
apply Zsqrtd.eq_of_smul_eq_smul_left hpprime.ne_zero
State after:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ ↑p.norm * a = ↑p.norm * ({ re := p.re, im := -↑A * p.im } * U)

State before:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ ↑p.norm * a = ↑p.norm * ({ re := p.re, im := -↑A * p.im } * U)
Tactic:
have : p.norm = p.re ^ 2 + 3 * (A : ℤ) ^ 2 * p.im ^ 2 :=
  by
  rw [Zsqrtd.norm_def, HAsq]
  ring
State after:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
this : p.norm = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ ↑p.norm * a = ↑p.norm * ({ re := p.re, im := -↑A * p.im } * U)

State before:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
this : p.norm = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ ↑p.norm * a = ↑p.norm * ({ re := p.re, im := -↑A * p.im } * U)
Tactic:
rw [mul_comm _ U, ← mul_assoc, ← HU, HX]
State after:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
this : p.norm = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ ↑p.norm * a =
    { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im } *
      { re := p.re, im := -↑A * p.im }

State before:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
this : p.norm = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ ↑p.norm * a =
    { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im } *
      { re := p.re, im := -↑A * p.im }
Tactic:
simp only [Zsqrtd.ext_iff, neg_mul, add_zero, Zsqrtd.intCast_re, MulZeroClass.zero_mul, mul_neg,
  Zsqrtd.mul_im, Zsqrtd.mul_re, neg_neg, MulZeroClass.mul_zero, neg_zero, Zsqrtd.intCast_im,
  this]
State after:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
this : p.norm = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ (p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2) * a.re =
      (p.re * a.re - ↑A * 3 * p.im * a.im) * p.re + 3 * (p.re * a.im + ↑A * a.re * p.im) * (↑A * p.im) ∧
    (p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2) * a.im =
      -((p.re * a.re - ↑A * 3 * p.im * a.im) * (↑A * p.im)) + (p.re * a.im + ↑A * a.re * p.im) * p.re

State before:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
this : p.norm = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ (p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2) * a.re =
      (p.re * a.re - ↑A * 3 * p.im * a.im) * p.re + 3 * (p.re * a.im + ↑A * a.re * p.im) * (↑A * p.im) ∧
    (p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2) * a.im =
      -((p.re * a.re - ↑A * 3 * p.im * a.im) * (↑A * p.im)) + (p.re * a.im + ↑A * a.re * p.im) * p.re
Tactic:
constructor <;> ring
State after:
no goals

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ ↑p.norm ∣ X
Tactic:
rw [Zsqrtd.intCast_dvd]
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ p.norm ∣ X.re ∧ p.norm ∣ X.im

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ p.norm ∣ X.re ∧ p.norm ∣ X.im
Tactic:
refine' ⟨_, HA⟩
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ p.norm ∣ X.re

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ p.norm ∣ X.re
Tactic:
apply @Prime.dvd_of_dvd_pow _ _ _ hpprime _ 2
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ p.norm ∣ X.re ^ 2

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ p.norm ∣ X.re ^ 2
Tactic:
have : X.re ^ 2 = X.norm - 3 * X.im ^ 2 :=
  by
  rw [Zsqrtd.norm_def]
  ring
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ p.norm ∣ X.re ^ 2

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ p.norm ∣ X.re ^ 2
Tactic:
rw [this]
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ p.norm ∣ X.norm - 3 * X.im ^ 2

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ p.norm ∣ X.norm - 3 * X.im ^ 2
Tactic:
apply dvd_sub
State after:
case h₁
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ p.norm ∣ X.norm

case h₂
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ p.norm ∣ 3 * X.im ^ 2

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ X.re ^ 2 = X.norm - 3 * X.im ^ 2
Tactic:
rw [Zsqrtd.norm_def]
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ X.re ^ 2 = X.re * X.re - -3 * X.im * X.im - 3 * X.im ^ 2

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
⊢ X.re ^ 2 = X.re * X.re - -3 * X.im * X.im - 3 * X.im ^ 2
Tactic:
ring
State after:
no goals

State before:
case h₁
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ p.norm ∣ X.norm
Tactic:
use a.norm
State after:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ X.norm = p.norm * a.norm

State before:
case h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ X.norm = p.norm * a.norm
Tactic:
trans
  (p.re * a.re) ^ 2 + (A : ℤ) ^ 2 * (3 * p.im * a.im) ^ 2 +
    3 * ((p.re * a.im) ^ 2 + (A : ℤ) ^ 2 * (a.re * p.im) ^ 2)
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ X.norm = (p.re * a.re) ^ 2 + ↑A ^ 2 * (3 * p.im * a.im) ^ 2 + 3 * ((p.re * a.im) ^ 2 + ↑A ^ 2 * (a.re * p.im) ^ 2)

a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ (p.re * a.re) ^ 2 + ↑A ^ 2 * (3 * p.im * a.im) ^ 2 + 3 * ((p.re * a.im) ^ 2 + ↑A ^ 2 * (a.re * p.im) ^ 2) =
    p.norm * a.norm

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ X.norm = (p.re * a.re) ^ 2 + ↑A ^ 2 * (3 * p.im * a.im) ^ 2 + 3 * ((p.re * a.im) ^ 2 + ↑A ^ 2 * (a.re * p.im) ^ 2)
Tactic:
simp only [Zsqrtd.norm_def]
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ (p.re * a.re - ↑A * 3 * p.im * a.im) * (p.re * a.re - ↑A * 3 * p.im * a.im) -
      -3 * (p.re * a.im + ↑A * a.re * p.im) * (p.re * a.im + ↑A * a.re * p.im) =
    (p.re * a.re) ^ 2 + ↑A ^ 2 * (3 * p.im * a.im) ^ 2 + 3 * ((p.re * a.im) ^ 2 + ↑A ^ 2 * (a.re * p.im) ^ 2)

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ (p.re * a.re - ↑A * 3 * p.im * a.im) * (p.re * a.re - ↑A * 3 * p.im * a.im) -
      -3 * (p.re * a.im + ↑A * a.re * p.im) * (p.re * a.im + ↑A * a.re * p.im) =
    (p.re * a.re) ^ 2 + ↑A ^ 2 * (3 * p.im * a.im) ^ 2 + 3 * ((p.re * a.im) ^ 2 + ↑A ^ 2 * (a.re * p.im) ^ 2)
Tactic:
ring
State after:
no goals

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ (p.re * a.re) ^ 2 + ↑A ^ 2 * (3 * p.im * a.im) ^ 2 + 3 * ((p.re * a.im) ^ 2 + ↑A ^ 2 * (a.re * p.im) ^ 2) =
    p.norm * a.norm
Tactic:
simp only [Zsqrtd.norm_def, HAsq]
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ (p.re * a.re) ^ 2 + 1 * (3 * p.im * a.im) ^ 2 + 3 * ((p.re * a.im) ^ 2 + 1 * (a.re * p.im) ^ 2) =
    (p.re * p.re - -3 * p.im * p.im) * (a.re * a.re - -3 * a.im * a.im)

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ (p.re * a.re) ^ 2 + 1 * (3 * p.im * a.im) ^ 2 + 3 * ((p.re * a.im) ^ 2 + 1 * (a.re * p.im) ^ 2) =
    (p.re * p.re - -3 * p.im * p.im) * (a.re * a.re - -3 * a.im * a.im)
Tactic:
ring
State after:
no goals

State before:
case h₂
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ p.norm ∣ 3 * X.im ^ 2
Tactic:
apply dvd_mul_of_dvd_right
State after:
case h₂.h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ p.norm ∣ X.im ^ 2

State before:
case h₂.h
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 = X.norm - 3 * X.im ^ 2
⊢ p.norm ∣ X.im ^ 2
Tactic:
exact dvd_pow HA two_ne_zero
State after:
no goals

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
this : a = { re := p.re, im := -↑A * p.im } * U
⊢ a = p * U ∨ a = star p * U
Tactic:
apply Or.imp _ _ (Int.units_eq_one_or A).symm <;> rintro rfl <;> simpa [Zsqrtd.ext] using this
State after:
no goals

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ p.norm = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
Tactic:
rw [Zsqrtd.norm_def, HAsq]
State after:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ p.re * p.re - -3 * p.im * p.im = p.re ^ 2 + 3 * 1 * p.im ^ 2

State before:
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ 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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ p.re * p.re - -3 * p.im * p.im = p.re ^ 2 + 3 * 1 * p.im ^ 2
Tactic:
ring
State after:
no goals