internlm/Lean-Github huggingface dataset:
Theorem: descent_gcd3
Proof state before:
case nonzero
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
⊢ ¬(s = 0 ∧ q = 0)
Tactic:
rintro ⟨h1, -⟩
Proof state after:
case nonzero.intro
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
h1 : s = 0
⊢ False
Theorem: descent_gcd3
Proof state before:
case nonzero.intro
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
h1 : s = 0
⊢ False
Tactic:
exact hspos h1
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
⊢ Even q ↔ ¬Even s
Tactic:
rw [Iff.comm, not_iff_comm, Iff.comm]
Proof state after:
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
⊢ Even s ↔ ¬Even q
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
⊢ Even s ↔ ¬Even q
Tactic:
have : ¬ Even (3 : ℤ) := by decide
Proof state after:
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
this : ¬Even 3
⊢ Even s ↔ ¬Even q
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
this : ¬Even 3
⊢ Even s ↔ ¬Even q
Tactic:
simpa [this, parity_simps] using hodd
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
⊢ ¬Even 3
Tactic:
decide
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
⊢ ∃ r, 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = r ^ 3
Tactic:
rcases hcube with (hcube | hcube | hcube) <;> [(use a); (use b); (use c)]
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
case inl
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
hcube : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3
⊢ ∃ r, 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = r ^ 3
Tactic:
use a
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
case inr.inl
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
hcube : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3
⊢ ∃ r, 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = r ^ 3
Tactic:
use b
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
case inr.inr
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
hcube : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ ∃ r, 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = r ^ 3
Tactic:
use c
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
⊢ Odd 3
Tactic:
norm_num
Proof state after:
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
⊢ ¬Even 3
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
⊢ ¬Even 3
Tactic:
decide
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 3 ^ 2 * 2 * s = d ^ 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
⊢ v ≠ 0
Tactic:
rintro rfl
Proof state after:
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 3 ^ 2 * 2 * s = d ^ 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u : ℤ
hq : q = u * (u - 3 * 0) * (u + 3 * 0)
hs : s = 3 * 0 * (u - 0) * (u + 0)
huvcoprime : IsCoprime u 0
huvodd : Even u ↔ ¬Even 0
⊢ False
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 3 ^ 2 * 2 * s = d ^ 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u : ℤ
hq : q = u * (u - 3 * 0) * (u + 3 * 0)
hs : s = 3 * 0 * (u - 0) * (u + 0)
huvcoprime : IsCoprime u 0
huvodd : Even u ↔ ¬Even 0
⊢ False
Tactic:
norm_num at hs
Proof state after:
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 3 ^ 2 * 2 * s = d ^ 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u : ℤ
hq : q = u * (u - 3 * 0) * (u + 3 * 0)
huvcoprime : IsCoprime u 0
huvodd : Even u ↔ ¬Even 0
hs : s = 0
⊢ False
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 3 ^ 2 * 2 * s = d ^ 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u : ℤ
hq : q = u * (u - 3 * 0) * (u + 3 * 0)
huvcoprime : IsCoprime u 0
huvodd : Even u ↔ ¬Even 0
hs : s = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
e : ℤ
he : 3 ^ 2 * 2 * s = e ^ 3
⊢ 3 ∣ e
Tactic:
rw [← Int.pow_dvd_pow_iff (by norm_num : 3 ≠ 0), ← he, hs]
Proof state after:
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
e : ℤ
he : 3 ^ 2 * 2 * s = e ^ 3
⊢ 3 ^ 3 ∣ 3 ^ 2 * 2 * (3 * v * (u - v) * (u + v))
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
e : ℤ
he : 3 ^ 2 * 2 * s = e ^ 3
⊢ 3 ^ 3 ∣ 3 ^ 2 * 2 * (3 * v * (u - v) * (u + v))
Tactic:
convert dvd_mul_right _ (2 * v * (u - v) * (u + v)) using 1
Proof state after:
case h.e'_4
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
e : ℤ
he : 3 ^ 2 * 2 * s = e ^ 3
⊢ 3 ^ 2 * 2 * (3 * v * (u - v) * (u + v)) = 3 ^ 3 * (2 * v * (u - v) * (u + v))
Theorem: descent_gcd3
Proof state before:
case h.e'_4
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
e : ℤ
he : 3 ^ 2 * 2 * s = e ^ 3
⊢ 3 ^ 2 * 2 * (3 * v * (u - v) * (u + v)) = 3 ^ 3 * (2 * v * (u - v) * (u + v))
Tactic:
norm_num
Proof state after:
case h.e'_4
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
e : ℤ
he : 3 ^ 2 * 2 * s = e ^ 3
⊢ 18 * (3 * v * (u - v) * (u + v)) = 27 * (2 * v * (u - v) * (u + v))
Theorem: descent_gcd3
Proof state before:
case h.e'_4
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
e : ℤ
he : 3 ^ 2 * 2 * s = e ^ 3
⊢ 18 * (3 * v * (u - v) * (u + v)) = 27 * (2 * v * (u - v) * (u + v))
Tactic:
ring
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
a b c q : ℤ
hq✝ : q ≠ 0
h3_ndvd_q : ¬3 ∣ q
s : ℤ
hp : 3 * s ≠ 0
hcoprime : IsCoprime (3 * s) q
hodd : Even (3 * s) ↔ ¬Even q
hcube :
  2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
    2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : (2 * (3 * s)).gcd ((3 * s) ^ 2 + 3 * q ^ 2) = 3
hspos : s ≠ 0
hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2)
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
r : ℤ
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
this : Odd 3
hcuberight : ∃ e, q ^ 2 + 3 * s ^ 2 = e ^ 3
u v : ℤ
hq : q = u * (u - 3 * v) * (u + 3 * v)
hs : s = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
hv : v ≠ 0
haddcoprime : IsCoprime (2 * v) (u + v)
hsubcoprime : IsCoprime (2 * v) (u - v)
haddsubcoprime : IsCoprime (u - v) (u + v)
e : ℤ
he : 3 ^ 2 * 2 * s = e ^ 3
⊢ 3 ≠ 0
Tactic:
norm_num
Proof state after:
no goals