internlm/Lean-Github huggingface dataset:
Theorem: factors2
Proof state before:
case inr.intro.inl
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re + a.im
⊢ ∃ b, a.norm = 4 * b.norm
Tactic:
obtain ⟨v, hv⟩ := h4
Proof state after:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ ∃ b, a.norm = 4 * b.norm
Theorem: factors2
Proof state before:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ ∃ b, a.norm = 4 * b.norm
Tactic:
use ⟨v - a.im, v⟩
Proof state after:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ a.norm = 4 * { re := v - a.im, im := v }.norm
Theorem: factors2
Proof state before:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ a.norm = 4 * { re := v - a.im, im := v }.norm
Tactic:
rw [eq_comm, ← sub_eq_iff_eq_add] at hv
Proof state after:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ a.norm = 4 * { re := v - a.im, im := v }.norm
Theorem: factors2
Proof state before:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ a.norm = 4 * { re := v - a.im, im := v }.norm
Tactic:
simp only [Zsqrtd.norm_def, ← hv]
Proof state after:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ (4 * v - a.im) * (4 * v - a.im) - -3 * a.im * a.im = 4 * ((v - a.im) * (v - a.im) - -3 * v * v)
Theorem: factors2
Proof state before:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ (4 * v - a.im) * (4 * v - a.im) - -3 * a.im * a.im = 4 * ((v - a.im) * (v - a.im) - -3 * v * v)
Tactic:
ring
Proof state after:
no goals
Theorem: factors2
Proof state before:
case inr.intro.inr
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re - a.im
⊢ ∃ b, a.norm = 4 * b.norm
Tactic:
obtain ⟨v, hv⟩ := h4
Proof state after:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ ∃ b, a.norm = 4 * b.norm
Theorem: factors2
Proof state before:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ ∃ b, a.norm = 4 * b.norm
Tactic:
use ⟨v + a.im, v⟩
Proof state after:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ a.norm = 4 * { re := v + a.im, im := v }.norm
Theorem: factors2
Proof state before:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ a.norm = 4 * { re := v + a.im, im := v }.norm
Tactic:
rw [sub_eq_iff_eq_add] at hv
Proof state after:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ a.norm = 4 * { re := v + a.im, im := v }.norm
Theorem: factors2
Proof state before:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ a.norm = 4 * { re := v + a.im, im := v }.norm
Tactic:
simp only [Zsqrtd.norm_def, hv]
Proof state after:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ (4 * v + a.im) * (4 * v + a.im) - -3 * a.im * a.im = 4 * ((v + a.im) * (v + a.im) - -3 * v * v)
Theorem: factors2
Proof state before:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ (4 * v + a.im) * (4 * v + a.im) - -3 * a.im * a.im = 4 * ((v + a.im) * (v + a.im) - -3 * v * v)
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
Tactic:
obtain ⟨f, hf⟩ := hdvd
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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
Proof 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)
Theorem: Spts.mul_of_dvd'
Proof 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
Proof 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)
Theorem: Spts.mul_of_dvd'
Proof 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)
Proof 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)
Theorem: Spts.mul_of_dvd'
Proof 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]
Proof 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)
Theorem: Spts.mul_of_dvd'
Proof 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
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
⊢ 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]
Proof 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)
Theorem: Spts.mul_of_dvd'
Proof 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
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, 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]
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof 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
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 + ↑(-1) * a.re * p.im
Theorem: Spts.mul_of_dvd'
Proof 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
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 + ↑1 * a.re * p.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
⊢ ↑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
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof 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
Proof 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
Theorem: Spts.mul_of_dvd'
Proof 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
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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ a = p * U ∨ a = star p * U
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 }
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
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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ a = { re := p.re, im := -↑A * p.im } * U
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 }
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
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 }
U : ℤ√(-3)
HU : X = ↑p.norm * U
⊢ ↑p.norm * a = ↑p.norm * ({ re := p.re, im := -↑A * p.im } * U)
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 }
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
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 }
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)
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 }
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]
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 }
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 }
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 }
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]
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 }
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
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 }
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
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 }
⊢ ↑p.norm ∣ X
Tactic:
rw [Zsqrtd.intCast_dvd]
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 }
⊢ p.norm ∣ X.re ∧ p.norm ∣ X.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 }
⊢ p.norm ∣ X.re ∧ p.norm ∣ X.im
Tactic:
refine' ⟨_, HA⟩
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 }
⊢ p.norm ∣ X.re
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 }
⊢ p.norm ∣ X.re
Tactic:
apply @Prime.dvd_of_dvd_pow _ _ _ hpprime _ 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 }
⊢ p.norm ∣ X.re ^ 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 }
⊢ p.norm ∣ 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 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