internlm/Lean-Github huggingface dataset:
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Tactic:
apply lt_of_lt_of_le (b := (2 * p * P.norm).natAbs)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (2 * p).natAbs < (2 * p * P.norm).natAbs

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (2 * p * P.norm).natAbs ≤ (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (2 * p).natAbs < (2 * p * P.norm).natAbs
Tactic:
rw [Int.natAbs_mul (2 * p)]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (2 * p).natAbs < (2 * p).natAbs * P.norm.natAbs
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (2 * p).natAbs < (2 * p).natAbs * P.norm.natAbs
Tactic:
apply lt_mul_of_one_lt_right (Int.natAbs_pos.mpr (mul_ne_zero two_ne_zero hp))
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ 1 < P.norm.natAbs
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ 1 < P.norm.natAbs
Tactic:
rw [← Int.ofNat_lt]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ ↑1 < ↑P.norm.natAbs
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ ↑1 < ↑P.norm.natAbs
Tactic:
rw [Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) P)]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ ↑1 < P.norm
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ ↑1 < P.norm
Tactic:
exact Spts.one_lt_of_im_ne_zero ⟨p, q⟩ hq
Proof state after:
no goals
Theorem: descent2
Proof state before:
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ -3 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (2 * p * P.norm).natAbs ≤ (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Tactic:
apply Nat.le_of_dvd
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.h
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ 0 < (a ^ 3 * b ^ 3 * c ^ 3).natAbs

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (2 * p * P.norm).natAbs ∣ (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.h
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ 0 < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Tactic:
rw [pos_iff_ne_zero, Int.natAbs_ne_zero, ← mul_pow, ← mul_pow]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.h
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (a * b * c) ^ 3 ≠ 0
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.h
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (a * b * c) ^ 3 ≠ 0
Tactic:
exact pow_ne_zero 3 (mul_ne_zero (mul_ne_zero hapos hbpos) hcpos)
Proof state after:
no goals
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (2 * p * P.norm).natAbs ∣ (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Tactic:
rw [Int.natAbs_dvd_natAbs]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ 2 * p * P.norm ∣ a ^ 3 * b ^ 3 * c ^ 3
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ 2 * p * P.norm ∣ a ^ 3 * b ^ 3 * c ^ 3
Tactic:
convert descent11 hcube
Proof state after:
case h.e'_3.h.e'_6
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ P.norm = p ^ 2 + 3 * q ^ 2
Theorem: descent2
Proof state before:
case h.e'_3.h.e'_6
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ P.norm = p ^ 2 + 3 * q ^ 2
Tactic:
rw [Zsqrtd.norm]
Proof state after:
case h.e'_3.h.e'_6
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ P.re * P.re - -3 * P.im * P.im = p ^ 2 + 3 * q ^ 2
Theorem: descent2
Proof state before:
case h.e'_3.h.e'_6
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ P.re * P.re - -3 * P.im * P.im = p ^ 2 + 3 * q ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
⊢ (2 * p).gcd (p ^ 2 + 3 * q ^ 2) = 1 ∨ (2 * p).gcd (p ^ 2 + 3 * q ^ 2) = 3
Tactic:
set g := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) with hg'
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
⊢ g = 1 ∨ g = 3
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
⊢ ∃ k, g = 3 ^ k ∧ k < 2
Tactic:
set k := g.factors.length
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ ∃ k, g = 3 ^ k ∧ k < 2
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ k
⊢ ∃ k, g = 3 ^ k ∧ k < 2
Tactic:
refine' ⟨k, hg, _⟩
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ k
⊢ k < 2
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ k
⊢ k < 2
Tactic:
by_contra! H
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ k
H : 2 ≤ k
⊢ False
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ k
H : 2 ≤ k
⊢ False
Tactic:
rw [← pow_mul_pow_sub _ H] at hg
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
⊢ False
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
⊢ False
Tactic:
have : ¬IsUnit (3 : ℤ) := by
  rw [Int.isUnit_iff_natAbs_eq]
  norm_num
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ False
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ False
Tactic:
apply this
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ IsUnit 3
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ IsUnit 3
Tactic:
have hdvdp : 3 ∣ p :=
  by
  suffices 3 ∣ 2 * p
    by
    apply Int.dvd_mul_cancel_prime' _ dvd_rfl Int.prime_two this
    norm_num
  have : 3 ∣ (g : ℤ) := by
    rw [hg, pow_two, mul_assoc, Int.ofNat_mul]
    apply dvd_mul_right
  exact dvd_trans this Int.gcd_dvd_left
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ∣ p
⊢ IsUnit 3
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ∣ p
⊢ IsUnit 3
Tactic:
apply IsCoprime.isUnit_of_dvd' hcoprime hdvdp
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ∣ p
⊢ 3 ∣ q
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
H : ∃ k, g = 3 ^ k ∧ k < 2
⊢ g = 1 ∨ g = 3
Tactic:
obtain ⟨k, hg, hk⟩ := H
Proof state after:
case intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ k
hk : k < 2
⊢ g = 1 ∨ g = 3
Theorem: gcd1or3
Proof state before:
case intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ k
hk : k < 2
⊢ g = 1 ∨ g = 3
Tactic:
interval_cases k
Proof state after:
case intro.intro.«0»
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 0
hk : 0 < 2
⊢ g = 1 ∨ g = 3

case intro.intro.«1»
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 1
hk : 1 < 2
⊢ g = 1 ∨ g = 3
Theorem: gcd1or3
Proof state before:
case intro.intro.«0»
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 0
hk : 0 < 2
⊢ g = 1 ∨ g = 3
Tactic:
left
Proof state after:
case intro.intro.«0».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 0
hk : 0 < 2
⊢ g = 1
Theorem: gcd1or3
Proof state before:
case intro.intro.«0».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 0
hk : 0 < 2
⊢ g = 1
Tactic:
rw [pow_zero] at hg
Proof state after:
case intro.intro.«0».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 1
hk : 0 < 2
⊢ g = 1
Theorem: gcd1or3
Proof state before:
case intro.intro.«0».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 1
hk : 0 < 2
⊢ g = 1
Tactic:
exact hg
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
case intro.intro.«1»
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 1
hk : 1 < 2
⊢ g = 1 ∨ g = 3
Tactic:
right
Proof state after:
case intro.intro.«1».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 1
hk : 1 < 2
⊢ g = 3
Theorem: gcd1or3
Proof state before:
case intro.intro.«1».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 1
hk : 1 < 2
⊢ g = 3
Tactic:
rw [pow_one] at hg
Proof state after:
case intro.intro.«1».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3
hk : 1 < 2
⊢ g = 3
Theorem: gcd1or3
Proof state before:
case intro.intro.«1».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3
hk : 1 < 2
⊢ g = 3
Tactic:
exact hg
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
⊢ ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
Tactic:
intro d hdprime hdleft hdright
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
⊢ d = 3
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
⊢ d = 3
Tactic:
by_contra hne3
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : ¬d = 3
⊢ False
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : ¬d = 3
⊢ False
Tactic:
rw [← Ne] at hne3
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
⊢ False
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
⊢ False
Tactic:
apply (Nat.prime_iff_prime_int.mp hdprime).not_unit
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
⊢ IsUnit ↑d