internlm/Lean-Github huggingface dataset:
Theorem: Spts.mul_of_dvd'
Proof state before:
case intro.intro.intro
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 }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
⊢ ↑(Zsqrtd.norm p) * a = ↑(Zsqrtd.norm p) * ({ 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
Proof state after:
case intro.intro.intro
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 }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
this : Zsqrtd.norm p = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ ↑(Zsqrtd.norm p) * a = ↑(Zsqrtd.norm p) * ({ re := p.re, im := -↑A * p.im } * U)
Theorem: Spts.mul_of_dvd'
Proof state before:
case intro.intro.intro
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 }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
this : Zsqrtd.norm p = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ ↑(Zsqrtd.norm p) * a = ↑(Zsqrtd.norm p) * ({ re := p.re, im := -↑A * p.im } * U)
Tactic:
rw [mul_comm _ U, ← mul_assoc, ← HU, HX]
Proof state after:
case intro.intro.intro
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 }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
this : Zsqrtd.norm p = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ ↑(Zsqrtd.norm p) * 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 }
Theorem: Spts.mul_of_dvd'
Proof state before:
case intro.intro.intro
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 }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
this : Zsqrtd.norm p = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
⊢ ↑(Zsqrtd.norm p) * 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, neg_mul, add_zero, Zsqrtd.coe_int_re, MulZeroClass.zero_mul, mul_neg,
  Zsqrtd.mul_im, Zsqrtd.mul_re, neg_neg, MulZeroClass.mul_zero, neg_zero, Zsqrtd.coe_int_im,
  this]
Proof state after:
case intro.intro.intro
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 }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
this : Zsqrtd.norm p = 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
Theorem: Spts.mul_of_dvd'
Proof state before:
case intro.intro.intro
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 }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
this : Zsqrtd.norm p = 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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof state before:
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 }
⊢ ↑(Zsqrtd.norm p) ∣ X
Tactic:
rw [Zsqrtd.coe_int_dvd_iff]
Proof state after:
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 }
⊢ Zsqrtd.norm p ∣ X.re ∧ Zsqrtd.norm p ∣ X.im
Theorem: Spts.mul_of_dvd'
Proof state before:
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 }
⊢ Zsqrtd.norm p ∣ X.re ∧ Zsqrtd.norm p ∣ X.im
Tactic:
refine' ⟨_, HA⟩
Proof state after:
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 }
⊢ Zsqrtd.norm p ∣ X.re
Theorem: Spts.mul_of_dvd'
Proof state before:
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 }
⊢ Zsqrtd.norm p ∣ X.re
Tactic:
apply @Prime.dvd_of_dvd_pow _ _ _ hpprime _ 2
Proof state after:
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 }
⊢ Zsqrtd.norm p ∣ X.re ^ 2
Theorem: Spts.mul_of_dvd'
Proof state before:
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 }
⊢ Zsqrtd.norm p ∣ X.re ^ 2
Tactic:
have : X.re ^ 2 = X.norm - 3 * X.im ^ 2 :=
  by
  rw [Zsqrtd.norm_def]
  ring
Proof state after:
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
Theorem: Spts.mul_of_dvd'
Proof state before:
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
Tactic:
rw [this]
Proof state after:
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
Theorem: Spts.mul_of_dvd'
Proof state before:
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
Tactic:
apply dvd_sub
Proof state after:
case h₁
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

case h₂
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 ∣ 3 * X.im ^ 2
Theorem: Spts.mul_of_dvd'
Proof state before:
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 }
⊢ X.re ^ 2 = Zsqrtd.norm X - 3 * X.im ^ 2
Tactic:
rw [Zsqrtd.norm_def]
Proof state after:
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 }
⊢ X.re ^ 2 = X.re * X.re - -3 * X.im * X.im - 3 * X.im ^ 2
Theorem: Spts.mul_of_dvd'
Proof state before:
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 }
⊢ X.re ^ 2 = X.re * X.re - -3 * X.im * X.im - 3 * X.im ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof state before:
case h₁
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
Tactic:
use a.norm
Proof state after:
case h₁
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 X = Zsqrtd.norm p * Zsqrtd.norm a
Theorem: Spts.mul_of_dvd'
Proof state before:
case h₁
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 X = Zsqrtd.norm p * Zsqrtd.norm a
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)
Proof state after:
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 X =
    (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 (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
⊢ (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) =
    Zsqrtd.norm p * Zsqrtd.norm a
Theorem: Spts.mul_of_dvd'
Proof state before:
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 X =
    (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]
Proof state after:
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
⊢ (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)
Theorem: Spts.mul_of_dvd'
Proof state before:
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
⊢ (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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof state before:
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
⊢ (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) =
    Zsqrtd.norm p * Zsqrtd.norm a
Tactic:
simp only [Zsqrtd.norm_def, HAsq]
Proof state after:
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
⊢ (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)
Theorem: Spts.mul_of_dvd'
Proof state before:
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
⊢ (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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof state before:
case h₂
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 ∣ 3 * X.im ^ 2
Tactic:
apply dvd_mul_of_dvd_right
Proof state after:
case h₂.h
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.im ^ 2
Theorem: Spts.mul_of_dvd'
Proof state before:
case h₂.h
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.im ^ 2
Tactic:
exact dvd_pow HA two_ne_zero
Proof state after:
no goals