internlm/Lean-Github huggingface dataset:
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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
x : ℤ := v * (u - v) * (u + v)
hx : x = v * (u - v) * (u + v)
⊢ (3 * x).natAbs = s.natAbs
Tactic:
rw [hx, 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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
x : ℤ := v * (u - v) * (u + v)
hx : x = v * (u - v) * (u + v)
⊢ (3 * (v * (u - v) * (u + v))).natAbs = (3 * v * (u - v) * (u + v)).natAbs
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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
x : ℤ := v * (u - v) * (u + v)
hx : x = v * (u - v) * (u + v)
⊢ (3 * (v * (u - v) * (u + v))).natAbs = (3 * v * (u - v) * (u + v)).natAbs
Tactic:
congr 1
Proof state after:
case e_m
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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
x : ℤ := v * (u - v) * (u + v)
hx : x = v * (u - v) * (u + v)
⊢ 3 * (v * (u - v) * (u + v)) = 3 * v * (u - v) * (u + v)
Theorem: descent_gcd3
Proof state before:
case e_m
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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
x : ℤ := v * (u - v) * (u + v)
hx : x = v * (u - v) * (u + v)
⊢ 3 * (v * (u - v) * (u + v)) = 3 * 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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
x : ℤ := v * (u - v) * (u + v)
hx : x = v * (u - v) * (u + v)
⊢ 0 < 2 * 3
Tactic:
norm_num
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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
x : ℤ := v * (u - v) * (u + v)
hx : x = v * (u - v) * (u + v)
⊢ 2 * 3 * s.natAbs = (2 * 3 * s).natAbs
Tactic:
rw [Int.natAbs_mul (2 * 3)]
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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
x : ℤ := v * (u - v) * (u + v)
hx : x = v * (u - v) * (u + v)
⊢ 2 * 3 * s.natAbs = (2 * 3).natAbs * s.natAbs
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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
x : ℤ := v * (u - v) * (u + v)
hx : x = v * (u - v) * (u + v)
⊢ 2 * 3 * s.natAbs = (2 * 3).natAbs * s.natAbs
Tactic:
rfl
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
⊢ A ^ 3 + B ^ 3 = C ^ 3
Tactic:
rw [← HA, ← HB, ← HC]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
⊢ 2 * v + (u - v) = u + v
Theorem: descent_gcd3
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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)
t : ℤ
he : 3 ^ 2 * 2 * s = (3 * t) ^ 3
ht : 2 * v * (u - v) * (u + v) = t ^ 3
A B C : ℤ
HApos : A ≠ 0
HBpos : B ≠ 0
HCpos : C ≠ 0
HA : 2 * v = A ^ 3
HB : u - v = B ^ 3
HC : u + v = C ^ 3
⊢ 2 * v + (u - v) = u + v
Tactic:
ring
Proof state after:
no goals
Theorem: descent
Proof state before:
a b c : ℤ
h : FltCoprime 3 a b c
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' * b' * c').natAbs < (a * b * c).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
have := descent2 a b c h
Proof state after:
a b c : ℤ
h : FltCoprime 3 a b c
this :
  ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (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) ∧
              (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' * b' * c').natAbs < (a * b * c).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent
Proof state before:
a b c : ℤ
h : FltCoprime 3 a b c
this :
  ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (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) ∧
              (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' * b' * c').natAbs < (a * b * c).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube, haaa⟩ := this
Proof state after:
case intro.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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' * b' * c').natAbs < (a * b * c).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent
Proof state before:
case intro.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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' * b' * c').natAbs < (a * b * c).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
suffices
  ∃ a' b' c' : ℤ,
    a' ≠ 0 ∧
      b' ≠ 0 ∧
        c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
  by
  obtain ⟨a', b', c', ha', hb', hc', hsmaller, hsolution⟩ := this
  refine' ⟨a', b', c', ha', hb', hc', _, hsolution⟩
  rw [← Nat.pow_lt_pow_iff_left three_ne_zero]
  convert lt_of_le_of_lt hsmaller haaa <;> simp [mul_pow, Int.natAbs_mul, Int.natAbs_pow]
Proof state after:
case intro.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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent
Proof state before:
case intro.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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
cases' gcd1or3 p q hp hcoprime hodd with hgcd hgcd
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.inl
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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
hgcd : (2 * p).gcd (p ^ 2 + 3 * q ^ 2) = 1
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

case intro.intro.intro.intro.intro.intro.intro.inr
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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
hgcd : (2 * p).gcd (p ^ 2 + 3 * q ^ 2) = 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent
Proof state before:
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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
this :
  ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' * b' * c').natAbs < (a * b * c).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
obtain ⟨a', b', c', ha', hb', hc', hsmaller, hsolution⟩ := this
Proof state after:
case intro.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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' * b' * c').natAbs < (a * b * c).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent
Proof state before:
case intro.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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' * b' * c').natAbs < (a * b * c).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
refine' ⟨a', b', c', ha', hb', hc', _, hsolution⟩
Proof state after:
case intro.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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ (a' * b' * c').natAbs < (a * b * c).natAbs
Theorem: descent
Proof state before:
case intro.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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ (a' * b' * c').natAbs < (a * b * c).natAbs
Tactic:
rw [← Nat.pow_lt_pow_iff_left three_ne_zero]
Proof state after:
case intro.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
haaa : (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ (a' * b' * c').natAbs ^ 3 < (a * b * c).natAbs ^ 3