internlm/Lean-Github huggingface dataset:
Theorem: Spts.mul_of_dvd'
Proof 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]
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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]
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof 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
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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)
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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]
Proof 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)
Theorem: Spts.mul_of_dvd'
Proof 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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof 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]
Proof 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)
Theorem: Spts.mul_of_dvd'
Proof 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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof 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
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof 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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof 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]
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd''
Proof state before:
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
⊢ ∃ u, (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Tactic:
obtain ⟨u, hu⟩ := Spts.mul_of_dvd' hdvd hpprime
Proof state after:
case intro
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ ∃ u, (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Theorem: Spts.mul_of_dvd''
Proof state before:
case intro
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ ∃ u, (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Tactic:
refine' ⟨u, hu, _⟩
Proof state after:
case intro
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ a.norm = p.norm * u.norm
Theorem: Spts.mul_of_dvd''
Proof state before:
case intro
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ a.norm = p.norm * u.norm
Tactic:
obtain rfl | rfl := hu
Proof state after:
case intro.inl
p : ℤ√(-3)
hpprime : Prime p.norm
u : ℤ√(-3)
hdvd : p.norm ∣ (p * u).norm
⊢ (p * u).norm = p.norm * u.norm

case intro.inr
p : ℤ√(-3)
hpprime : Prime p.norm
u : ℤ√(-3)
hdvd : p.norm ∣ (star p * u).norm
⊢ (star p * u).norm = p.norm * u.norm
Theorem: Spts.mul_of_dvd''
Proof state before:
case intro.inl
p : ℤ√(-3)
hpprime : Prime p.norm
u : ℤ√(-3)
hdvd : p.norm ∣ (p * u).norm
⊢ (p * u).norm = p.norm * u.norm
Tactic:
rw [Zsqrtd.norm_mul]
Proof state after:
no goals
Theorem: Spts.mul_of_dvd''
Proof state before:
case intro.inr
p : ℤ√(-3)
hpprime : Prime p.norm
u : ℤ√(-3)
hdvd : p.norm ∣ (star p * u).norm
⊢ (star p * u).norm = p.norm * u.norm
Tactic:
rw [Zsqrtd.norm_mul, Zsqrtd.norm_conj]
Proof state after:
no goals
Theorem: factors'
Proof state before:
a : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
⊢ ∃ p, |f| = p.norm
Tactic:
induction' hg : g.natAbs using Nat.strong_induction_on with g'' IH generalizing a g
Proof state after:
case h
f : ℤ
hodd : Odd f
g'' : ℕ
IH :
  ∀ m < g'',
    ∀ (a : ℤ√(-3)) (g : ℤ),
      g ≠ 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
hg : g.natAbs = g''
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case h
f : ℤ
hodd : Odd f
g'' : ℕ
IH :
  ∀ m < g'',
    ∀ (a : ℤ√(-3)) (g : ℤ),
      g ≠ 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
hg : g.natAbs = g''
⊢ ∃ p, |f| = p.norm
Tactic:
subst g''
Proof state after:
case h
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      g ≠ 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case h
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      g ≠ 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
⊢ ∃ p, |f| = p.norm
Tactic:
dsimp at IH
Proof state after:
case h
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case h
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
⊢ ∃ p, |f| = p.norm
Tactic:
by_cases H : Even (Zsqrtd.norm a)
Proof state after:
case pos
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
H : Even a.norm
⊢ ∃ p, |f| = p.norm

case neg
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
H : ¬Even a.norm
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case pos
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
H : Even a.norm
⊢ ∃ p, |f| = p.norm
Tactic:
obtain ⟨c, hc⟩ := factors2 H
Proof state after:
case pos.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case pos.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
this : 4 ∣ g
⊢ ∃ p, |f| = p.norm
Tactic:
obtain ⟨g', rfl⟩ := this
Proof state after:
case pos.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * g').natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case pos.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * g').natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
⊢ ∃ p, |f| = p.norm
Tactic:
have hg'pos : g' ≠ 0 := right_ne_zero_of_mul hgpos
Proof state after:
case pos.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * g').natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
hg'pos : g' ≠ 0
⊢ ∃ p, |f| = p.norm