internlm/Lean-Github huggingface dataset:
Theorem: descent_gcd3
Proof state before:
case hc.a
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 : Int.gcd (2 * (3 * s)) ((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
H : u = -v
⊢ ?hc.a ↔ ¬?hc.a

case hc.a
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 : Int.gcd (2 * (3 * s)) ((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
H : u = -v
⊢ Prop
Tactic:
simpa [H, parity_simps] using huvodd
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
case hcoprimeab
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 : Int.gcd (2 * (3 * s)) ((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
⊢ IsCoprime (2 * v) (u - v)
Tactic:
exact hsubcoprime
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
case hcoprimeac
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 : Int.gcd (2 * (3 * s)) ((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
⊢ IsCoprime (2 * v) (u + v)
Tactic:
exact haddcoprime
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
case hcoprimebc
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 : Int.gcd (2 * (3 * s)) ((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
⊢ IsCoprime (u - v) (u + v)
Tactic:
exact haddsubcoprime
Proof state after:
no goals
Theorem: descent_gcd3
Proof state before:
case hs
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 : Int.gcd (2 * (3 * s)) ((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
⊢ 2 * v * (u - v) * (u + v) = ?s ^ 3
Tactic:
exact ht
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'_1
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 : Int.gcd (2 * (3 * s)) ((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
⊢ Int.natAbs (A ^ 3 * B ^ 3 * C ^ 3) ≤ Int.natAbs (2 * (3 * s))
Tactic:
rw [← mul_assoc, mul_comm, ← mul_assoc (C ^ 3), ← 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'_1
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 : Int.gcd (2 * (3 * s)) ((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
⊢ Int.natAbs ((u + v) * (2 * v) * (u - v)) ≤ Int.natAbs (2 * 3 * s)
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'_1
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 : Int.gcd (2 * (3 * s)) ((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
⊢ Int.natAbs ((u + v) * (2 * v) * (u - v)) ≤ Int.natAbs (2 * 3 * s)
Tactic:
set x := v * (u - v) * (u + v) with hx
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'_1
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 : Int.gcd (2 * (3 * s)) ((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)
⊢ Int.natAbs ((u + v) * (2 * v) * (u - v)) ≤ Int.natAbs (2 * 3 * s)
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'_1
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 : Int.gcd (2 * (3 * s)) ((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)
⊢ Int.natAbs ((u + v) * (2 * v) * (u - v)) ≤ Int.natAbs (2 * 3 * s)
Tactic:
calc
  ((u + v) * (2 * v) * (u - v)).natAbs = (2 * x).natAbs :=
    by
    rw [hx]
    congr 1
    ring
  _ = 2 * x.natAbs := by
    rw [Int.natAbs_mul 2]
    rfl
  _ ≤ 3 * x.natAbs := (Nat.mul_le_mul_right _ (by norm_num))
  _ = (3 * x).natAbs := by
    rw [Int.natAbs_mul 3]
    rfl
  _ = s.natAbs := by
    rw [hx, hs]
    congr 1
    ring
  _ ≤ 2 * 3 * s.natAbs := (Nat.le_mul_of_pos_left (by norm_num))
  _ = (2 * 3 * s).natAbs := by
    rw [Int.natAbs_mul (2 * 3)]
    rfl
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 : Int.gcd (2 * (3 * s)) ((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)
⊢ Int.natAbs ((u + v) * (2 * v) * (u - v)) = Int.natAbs (2 * x)
Tactic:
rw [hx]
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 : Int.gcd (2 * (3 * s)) ((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)
⊢ Int.natAbs ((u + v) * (2 * v) * (u - v)) = Int.natAbs (2 * (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 : Int.gcd (2 * (3 * s)) ((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)
⊢ Int.natAbs ((u + v) * (2 * v) * (u - v)) = Int.natAbs (2 * (v * (u - v) * (u + v)))
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 : Int.gcd (2 * (3 * s)) ((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)
⊢ (u + v) * (2 * v) * (u - v) = 2 * (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 : Int.gcd (2 * (3 * s)) ((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)
⊢ (u + v) * (2 * v) * (u - v) = 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 : Int.gcd (2 * (3 * s)) ((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)
⊢ Int.natAbs (2 * x) = 2 * Int.natAbs x
Tactic:
rw [Int.natAbs_mul 2]
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 : Int.gcd (2 * (3 * s)) ((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)
⊢ Int.natAbs 2 * Int.natAbs x = 2 * Int.natAbs x