Theorem: descent_gcd1
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a b c p q : ℤ
hp : p ≠ 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
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this✝² : Odd 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
u v : ℤ
hpfactor : p = u * (u - 3 * v) * (u + 3 * v)
hq : q = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
u_ne_zero : u ≠ 0
haaa : 2 * p = 2 * u * (u - 3 * v) * (u + 3 * v)
this✝¹ : ¬Even 3
this✝ : ¬Even (u - 3 * v)
this : ¬Even (u + 3 * v)
notdvd_2_2 : ¬2 ∣ u - 3 * v
hddd : ¬3 ∣ p
not_3_dvd_2 : ¬3 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
s : ℤ
hs : 2 * p = s ^ 3
C A B : ℤ
HCpos : C ≠ 0
HApos : A ≠ 0
HBpos : B ≠ 0
HC : 2 * u = C ^ 3
HA : u - 3 * v = A ^ 3
HB : u + 3 * v = B ^ 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
Tactic:
refine' ⟨A, B, C, HApos, HBpos, HCpos, _, _⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
a b c p q : ℤ
hp : p ≠ 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
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this✝² : Odd 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
u v : ℤ
hpfactor : p = u * (u - 3 * v) * (u + 3 * v)
hq : q = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
u_ne_zero : u ≠ 0
haaa : 2 * p = 2 * u * (u - 3 * v) * (u + 3 * v)
this✝¹ : ¬Even 3
this✝ : ¬Even (u - 3 * v)
this : ¬Even (u + 3 * v)
notdvd_2_2 : ¬2 ∣ u - 3 * v
hddd : ¬3 ∣ p
not_3_dvd_2 : ¬3 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
s : ℤ
hs : 2 * p = s ^ 3
C A B : ℤ
HCpos : C ≠ 0
HApos : A ≠ 0
HBpos : B ≠ 0
HC : 2 * u = C ^ 3
HA : u - 3 * v = A ^ 3
HB : u + 3 * v = B ^ 3
⊢ (A ^ 3 * B ^ 3 * C ^ 3).natAbs ≤ (2 * p).natAbs

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
a b c p q : ℤ
hp : p ≠ 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
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this✝² : Odd 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
u v : ℤ
hpfactor : p = u * (u - 3 * v) * (u + 3 * v)
hq : q = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
u_ne_zero : u ≠ 0
haaa : 2 * p = 2 * u * (u - 3 * v) * (u + 3 * v)
this✝¹ : ¬Even 3
this✝ : ¬Even (u - 3 * v)
this : ¬Even (u + 3 * v)
notdvd_2_2 : ¬2 ∣ u - 3 * v
hddd : ¬3 ∣ p
not_3_dvd_2 : ¬3 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
s : ℤ
hs : 2 * p = s ^ 3
C A B : ℤ
HCpos : C ≠ 0
HApos : A ≠ 0
HBpos : B ≠ 0
HC : 2 * u = C ^ 3
HA : u - 3 * v = A ^ 3
HB : u + 3 * v = B ^ 3
⊢ A ^ 3 + B ^ 3 = C ^ 3