internlm/Lean-Github huggingface dataset:
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro
a b c : ℤ
h : FltCoprime 3 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
⊢ Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
Tactic:
obtain ⟨⟨hapos, hbpos, hcpos, -⟩, -⟩ := h
Proof state after:
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
⊢ Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
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
⊢ Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
Tactic:
set P : ℤ√(-3) := ⟨p, q⟩
Proof state after:
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 }
⊢ Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
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 }
⊢ Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
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 }
⊢ Int.natAbs (2 * p) < Int.natAbs (2 * p * Zsqrtd.norm P)

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 }
⊢ Int.natAbs (2 * p * Zsqrtd.norm P) ≤ Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
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 }
⊢ Int.natAbs (2 * p) < Int.natAbs (2 * p * Zsqrtd.norm P)
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 }
⊢ Int.natAbs (2 * p) < Int.natAbs (2 * p) * Int.natAbs (Zsqrtd.norm P)
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 }
⊢ Int.natAbs (2 * p) < Int.natAbs (2 * p) * Int.natAbs (Zsqrtd.norm P)
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 < Int.natAbs (Zsqrtd.norm P)
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 < Int.natAbs (Zsqrtd.norm P)
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 < ↑(Int.natAbs (Zsqrtd.norm P))
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 < ↑(Int.natAbs (Zsqrtd.norm P))
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 < Zsqrtd.norm P
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 < Zsqrtd.norm P
Tactic:
exact Spts.one_lt_of_im_ne_zero ⟨p, q⟩ hq
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 }
⊢ Int.natAbs (2 * p * Zsqrtd.norm P) ≤ Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
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 < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)

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 }
⊢ Int.natAbs (2 * p * Zsqrtd.norm P) ∣ Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
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 < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
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.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 }
⊢ Int.natAbs (2 * p * Zsqrtd.norm P) ∣ Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
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 * Zsqrtd.norm P ∣ 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 * Zsqrtd.norm P ∣ 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 }
⊢ Zsqrtd.norm P = 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 }
⊢ Zsqrtd.norm P = 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: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
⊢ Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 1 ∨ Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
⊢ g = 1 ∨ g = 3
Tactic:
suffices H : ∃ k, g = 3 ^ k ∧ k < 2
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
H : ∃ k, g = 3 ^ k ∧ k < 2
⊢ g = 1 ∨ g = 3

case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
⊢ ∃ k, g = 3 ^ k ∧ k < 2
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑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:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ ∃ k, g = 3 ^ k ∧ k < 2
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ k
⊢ ∃ k, g = 3 ^ k ∧ k < 2
Tactic:
refine' ⟨k, hg, _⟩
Proof state after:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ k
⊢ k < 2
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ k
⊢ k < 2
Tactic:
by_contra' H
Proof state after:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ k
H : 2 ≤ List.length (Nat.factors g)
⊢ False
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ k
H : 2 ≤ List.length (Nat.factors g)
⊢ False
Tactic:
rw [← pow_mul_pow_sub _ H] at hg
Proof state after:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
⊢ False
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
⊢ False
Tactic:
have : ¬IsUnit (3 : ℤ) := by
  rw [Int.isUnit_iff_natAbs_eq]
  norm_num
Proof state after:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
⊢ False
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
⊢ False
Tactic:
apply this
Proof state after:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
⊢ IsUnit 3
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
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:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ∣ p
⊢ IsUnit 3
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ∣ p
⊢ IsUnit 3
Tactic:
apply IsCoprime.isUnit_of_dvd' hcoprime hdvdp
Proof state after:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
⊢ ∀ (f : ℕ), Nat.Prime f → ↑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 : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : Nat.Prime d
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
⊢ d = 3