Theorem: descent (Flt/Euler.lean)

State before:
a b c : ℤ
h : FltCoprime 3 a b c
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
have := descent2 a b c h
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) ∧
              Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

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) ∧
              Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube, haaa⟩ := this
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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c) ∧ 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_iff_lt_left (by norm_num : 1 ≤ 3)]
  convert lt_of_le_of_lt hsmaller haaa <;> simp [mul_pow, Int.natAbs_mul, Int.natAbs_pow]
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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
⊢ ∃ a' b' c',
    a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
⊢ ∃ a' b' c',
    a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
cases' gcd1or3 p q hp hcoprime hodd with hgcd hgcd
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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
hgcd : Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 1
⊢ ∃ a' b' c',
    a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ 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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
hgcd : Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 3
⊢ ∃ a' b' c',
    a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
this :
  ∃ a' b' c',
    a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
obtain ⟨a', b', c', ha', hb', hc', hsmaller, hsolution⟩ := this
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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p)
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p)
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
refine' ⟨a', b', c', ha', hb', hc', _, hsolution⟩
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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p)
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c)

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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p)
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c)
Tactic:
rw [← Nat.pow_lt_iff_lt_left (by norm_num : 1 ≤ 3)]
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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p)
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ Int.natAbs (a' * b' * c') ^ 3 < Int.natAbs (a * b * c) ^ 3

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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p)
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ Int.natAbs (a' * b' * c') ^ 3 < Int.natAbs (a * b * c) ^ 3
Tactic:
convert lt_of_le_of_lt hsmaller haaa <;> simp [mul_pow, Int.natAbs_mul, Int.natAbs_pow]
State after:
no goals

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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
a' b' c' : ℤ
ha' : a' ≠ 0
hb' : b' ≠ 0
hc' : c' ≠ 0
hsmaller : Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p)
hsolution : a' ^ 3 + b' ^ 3 = c' ^ 3
⊢ 1 ≤ 3
Tactic:
norm_num
State after:
no goals

State before:
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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
hgcd : Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 1
⊢ ∃ a' b' c',
    a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
rw [Int.gcd_eq_one_iff_coprime] at hgcd
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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
⊢ ∃ a' b' c',
    a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

State before:
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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
⊢ ∃ a' b' c',
    a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
apply descent_gcd1 a b c p q hp hcoprime hodd hcube hgcd
State after:
no goals

State before:
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 : Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
hgcd : Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 3
⊢ ∃ a' b' c',
    a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
apply descent_gcd3 a b c p q hp hq hcoprime hodd hcube hgcd
State after:
no goals