Theorem: descent_gcd3
Proof state before:
case intro.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 : 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 : ?m.138743
hr : 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) = r ^ 3
⊢ ∃ a' b' c',
    a' ≠ 0 ∧
      b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * (3 * s)) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

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)
⊢ Type ?u.138629

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)
⊢ ?m.138743 → Type ?u.138628

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 : ?m.138743) → HPow ?m.138743 (?m.138939 r) ℤ

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 : ?m.138743) → OfNat (?m.138939 r) 3
Tactic:
have : Odd 3 := by norm_num
Proof state after:
case intro.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 : 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
⊢ ∃ a' b' c',
    a' ≠ 0 ∧
      b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * (3 * s)) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3