internlm/Lean-Github huggingface dataset:
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 : 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]
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 : 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
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 : 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
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 : 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
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 : 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
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 : 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
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 : 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⟩
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 : 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)
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 : 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)]
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 : 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
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 : 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]
Proof state after:
no goals
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 : 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
Proof state after:
no goals
Theorem: descent
Proof 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
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 : 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
Theorem: descent
Proof 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
Proof state after:
no goals
Theorem: descent
Proof 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
Proof state after:
no goals
Theorem: flt_three
Proof state before:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
Tactic:
induction' h : (a * b * c).natAbs using Nat.strong_induction_on with k' IH generalizing a b c
Proof state after:
case h
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
Theorem: flt_three
Proof state before:
case h
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
Tactic:
intro H
Proof state after:
case h
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
⊢ False
Theorem: flt_three
Proof state before:
case h
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
⊢ False
Tactic:
obtain ⟨x'', y'', z'', hxle, hyle, hzle, hcoprime⟩ := exists_coprime zero_lt_three ha hb hc H
Proof state after:
case h.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
⊢ False
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
⊢ False
Tactic:
obtain ⟨x', y', z', hx'pos, hy'pos, hz'pos, hsmaller, hsolution⟩ := descent x'' y'' z'' hcoprime
Proof state after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ False
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ False
Tactic:
refine' IH (x' * y' * z').natAbs _ hx'pos hy'pos hz'pos rfl hsolution
Proof state after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x' * y' * z') < k'
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x' * y' * z') < k'
Tactic:
apply lt_of_lt_of_le hsmaller
Proof state after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x'' * y'' * z'') ≤ k'
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x'' * y'' * z'') ≤ k'
Tactic:
rw [← h]
Proof state after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x'' * y'' * z'') ≤ Int.natAbs (a * b * c)
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs (x'' * y'' * z'') ≤ Int.natAbs (a * b * c)
Tactic:
simp only [Int.natAbs_mul]
Proof state after:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs x'' * Int.natAbs y'' * Int.natAbs z'' ≤ Int.natAbs a * Int.natAbs b * Int.natAbs c
Theorem: flt_three
Proof state before:
case h.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
x'' y'' z'' : ℤ
hxle : Int.natAbs x'' ≤ Int.natAbs a
hyle : Int.natAbs y'' ≤ Int.natAbs b
hzle : Int.natAbs z'' ≤ Int.natAbs c
hcoprime : FltCoprime 3 x'' y'' z''
x' y' z' : ℤ
hx'pos : x' ≠ 0
hy'pos : y' ≠ 0
hz'pos : z' ≠ 0
hsmaller : Int.natAbs (x' * y' * z') < Int.natAbs (x'' * y'' * z'')
hsolution : x' ^ 3 + y' ^ 3 = z' ^ 3
⊢ Int.natAbs x'' * Int.natAbs y'' * Int.natAbs z'' ≤ Int.natAbs a * Int.natAbs b * Int.natAbs c
Tactic:
exact Nat.mul_le_mul (Nat.mul_le_mul hxle hyle) hzle
Proof state after:
no goals
Theorem: OddPrimeOrFour.ne_zero
Proof state before:
z : ℤ
h : OddPrimeOrFour z
⊢ z ≠ 0
Tactic:
obtain rfl | ⟨h, -⟩ := h
Proof state after:
case inl

⊢ 4 ≠ 0

case inr.intro
z : ℤ
h : Prime z
⊢ z ≠ 0
Theorem: OddPrimeOrFour.ne_zero
Proof state before:
case inr.intro
z : ℤ
h : Prime z
⊢ z ≠ 0
Tactic:
exact h.ne_zero
Proof state after:
no goals
Theorem: OddPrimeOrFour.ne_one
Proof state before:
z : ℤ
h : OddPrimeOrFour z
⊢ z ≠ 1
Tactic:
obtain rfl | ⟨h, -⟩ := h
Proof state after:
case inl

⊢ 4 ≠ 1

case inr.intro
z : ℤ
h : Prime z
⊢ z ≠ 1
Theorem: OddPrimeOrFour.ne_one
Proof state before:
case inr.intro
z : ℤ
h : Prime z
⊢ z ≠ 1
Tactic:
exact h.ne_one
Proof state after:
no goals
Theorem: OddPrimeOrFour.one_lt_abs
Proof state before:
z : ℤ
h : OddPrimeOrFour z
⊢ 1 < abs z
Tactic:
obtain rfl | ⟨h, -⟩ := h
Proof state after:
case inl

⊢ 1 < abs 4

case inr.intro
z : ℤ
h : Prime z
⊢ 1 < abs z
Theorem: OddPrimeOrFour.one_lt_abs
Proof state before:
case inl

⊢ 1 < abs 4
Tactic:
rw [Int.abs_eq_natAbs]
Proof state after:
case inl

⊢ 1 < ↑(Int.natAbs 4)
Theorem: OddPrimeOrFour.one_lt_abs
Proof state before:
case inl

⊢ 1 < ↑(Int.natAbs 4)
Tactic:
norm_num
Proof state after:
no goals
Theorem: OddPrimeOrFour.one_lt_abs
Proof state before:
case inr.intro
z : ℤ
h : Prime z
⊢ 1 < abs z
Tactic:
rw [Int.abs_eq_natAbs]
Proof state after:
case inr.intro
z : ℤ
h : Prime z
⊢ 1 < ↑(Int.natAbs z)
Theorem: OddPrimeOrFour.one_lt_abs
Proof state before:
case inr.intro
z : ℤ
h : Prime z
⊢ 1 < ↑(Int.natAbs z)
Tactic:
rw [Int.prime_iff_natAbs_prime] at h
Proof state after:
case inr.intro
z : ℤ
h : Nat.Prime (Int.natAbs z)
⊢ 1 < ↑(Int.natAbs z)
Theorem: OddPrimeOrFour.one_lt_abs
Proof state before:
case inr.intro
z : ℤ
h : Nat.Prime (Int.natAbs z)
⊢ 1 < ↑(Int.natAbs z)
Tactic:
norm_cast
Proof state after:
case inr.intro
z : ℤ
h : Nat.Prime (Int.natAbs z)
⊢ 1 < Int.natAbs z
Theorem: OddPrimeOrFour.one_lt_abs
Proof state before:
case inr.intro
z : ℤ
h : Nat.Prime (Int.natAbs z)
⊢ 1 < Int.natAbs z
Tactic:
exact h.one_lt
Proof state after:
no goals
Theorem: OddPrimeOrFour.not_unit
Proof state before:
z : ℤ
h : OddPrimeOrFour z
⊢ ¬IsUnit z
Tactic:
obtain rfl | ⟨h, -⟩ := h
Proof state after:
case inl

⊢ ¬IsUnit 4

case inr.intro
z : ℤ
h : Prime z
⊢ ¬IsUnit z
Theorem: OddPrimeOrFour.not_unit
Proof state before:
case inr.intro
z : ℤ
h : Prime z
⊢ ¬IsUnit z
Tactic:
exact h.not_unit
Proof state after:
no goals