internlm/Lean-Github huggingface dataset:
Theorem: Imo1981P3.ProblemPredicate.reduction
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
⊢ n - m ∈ Ioc 0 ↑N
Tactic:
have h5 : 0 < n - m := sub_pos.mpr h3
Proof state after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
⊢ n - m ∈ Ioc 0 ↑N
Theorem: Imo1981P3.ProblemPredicate.reduction
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
⊢ n - m ∈ Ioc 0 ↑N
Tactic:
have h6 : n - m < N := by
  calc
    _ < n := sub_lt_self n h1.m_range.left
    _ ≤ N := h1.n_range.right
Proof state after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
h6 : n - m < ↑N
⊢ n - m ∈ Ioc 0 ↑N
Theorem: Imo1981P3.ProblemPredicate.reduction
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
h6 : n - m < ↑N
⊢ n - m ∈ Ioc 0 ↑N
Tactic:
exact ⟨h5, h6.le⟩
Proof state after:
no goals
Theorem: Imo1981P3.ProblemPredicate.reduction
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
⊢ n - m < ↑N
Tactic:
calc
  _ < n := sub_lt_self n h1.m_range.left
  _ ≤ N := h1.n_range.right
Proof state after:
no goals
Theorem: Imo1981P3.ProblemPredicate.reduction
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
⊢ (m ^ 2 - (n - m) * m - (n - m) ^ 2) ^ 2 = 1
Tactic:
linear_combination h1.eq_one
Proof state after:
no goals
Theorem: Imo1981P3.NatPredicate.reduction
Proof state before:
N m n : ℕ
h1 : NatPredicate N m n
h2 : 1 < n
⊢ NatPredicate N (n - m) m
Tactic:
have : m ≤ n := h1.m_le_n
Proof state after:
N m n : ℕ
h1 : NatPredicate N m n
h2 : 1 < n
this : m ≤ n
⊢ NatPredicate N (n - m) m
Theorem: Imo1981P3.NatPredicate.reduction
Proof state before:
N m n : ℕ
h1 : NatPredicate N m n
h2 : 1 < n
this : m ≤ n
⊢ NatPredicate N (n - m) m
Tactic:
exact mod_cast h1.reduction (mod_cast h2)
Proof state after:
no goals
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
N n : ℕ
⊢ ∀ (m : ℕ), NatPredicate N m n → ∃ k, m = k.fib ∧ n = (k + 1).fib
Tactic:
refine Nat.strong_induction_on n ?_
Proof state after:
N n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib) →
      ∀ (m : ℕ), NatPredicate N m n → ∃ k, m = k.fib ∧ n = (k + 1).fib
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
N n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib) →
      ∀ (m : ℕ), NatPredicate N m n → ∃ k, m = k.fib ∧ n = (k + 1).fib
Tactic:
intro n h1 m h2
Proof state after:
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
Tactic:
have h3 : m ≤ n := h2.m_le_n
Proof state after:
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
h3 : m ≤ n
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
h3 : m ≤ n
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
Tactic:
obtain (rfl : 1 = n) | (h4 : 1 < n) := (succ_le_iff.mpr h2.n_pos).eq_or_lt
Proof state after:
case inl
N n m : ℕ
h1 : ∀ m < 1, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h2 : NatPredicate N m 1
h3 : m ≤ 1
⊢ ∃ k, m = k.fib ∧ 1 = (k + 1).fib

case inr
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
h3 : m ≤ n
h4 : 1 < n
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
case inl
N n m : ℕ
h1 : ∀ m < 1, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h2 : NatPredicate N m 1
h3 : m ≤ 1
⊢ ∃ k, m = k.fib ∧ 1 = (k + 1).fib
Tactic:
use 1
Proof state after:
case h
N n m : ℕ
h1 : ∀ m < 1, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h2 : NatPredicate N m 1
h3 : m ≤ 1
⊢ m = fib 1 ∧ 1 = (1 + 1).fib
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
case h
N n m : ℕ
h1 : ∀ m < 1, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h2 : NatPredicate N m 1
h3 : m ≤ 1
⊢ m = fib 1 ∧ 1 = (1 + 1).fib
Tactic:
have h5 : 1 ≤ m := succ_le_iff.mpr h2.m_pos
Proof state after:
case h
N n m : ℕ
h1 : ∀ m < 1, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h2 : NatPredicate N m 1
h3 : m ≤ 1
h5 : 1 ≤ m
⊢ m = fib 1 ∧ 1 = (1 + 1).fib
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
case h
N n m : ℕ
h1 : ∀ m < 1, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h2 : NatPredicate N m 1
h3 : m ≤ 1
h5 : 1 ≤ m
⊢ m = fib 1 ∧ 1 = (1 + 1).fib
Tactic:
simpa [fib_one, fib_two, (by decide : 1 + 1 = 2)] using (h3.antisymm h5 : m = 1)
Proof state after:
no goals
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
N n m : ℕ
h1 : ∀ m < 1, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h2 : NatPredicate N m 1
h3 : m ≤ 1
h5 : 1 ≤ m
⊢ 1 + 1 = 2
Tactic:
decide
Proof state after:
no goals
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
case inr
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
h3 : m ≤ n
h4 : 1 < n
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
Tactic:
obtain (rfl : m = n) | (h6 : m < n) := h3.eq_or_lt
Proof state after:
case inr.inl
N n m : ℕ
h1 : ∀ m_1 < m, ∀ (m : ℕ), NatPredicate N m m_1 → ∃ k, m = k.fib ∧ m_1 = (k + 1).fib
h2 : NatPredicate N m m
h3 : m ≤ m
h4 : 1 < m
⊢ ∃ k, m = k.fib ∧ m = (k + 1).fib

case inr.inr
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
h3 : m ≤ n
h4 : 1 < n
h6 : m < n
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
case inr.inl
N n m : ℕ
h1 : ∀ m_1 < m, ∀ (m : ℕ), NatPredicate N m m_1 → ∃ k, m = k.fib ∧ m_1 = (k + 1).fib
h2 : NatPredicate N m m
h3 : m ≤ m
h4 : 1 < m
⊢ ∃ k, m = k.fib ∧ m = (k + 1).fib
Tactic:
exact absurd h2.eq_imp_1 (Nat.ne_of_gt h4)
Proof state after:
no goals
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
case inr.inr
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
h3 : m ≤ n
h4 : 1 < n
h6 : m < n
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
Tactic:
have h7 : NatPredicate N (n - m) m := h2.reduction h4
Proof state after:
case inr.inr
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
h3 : m ≤ n
h4 : 1 < n
h6 : m < n
h7 : NatPredicate N (n - m) m
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
case inr.inr
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
h3 : m ≤ n
h4 : 1 < n
h6 : m < n
h7 : NatPredicate N (n - m) m
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
Tactic:
obtain ⟨k : ℕ, hnm : n - m = fib k, rfl : m = fib (k + 1)⟩ := h1 m h6 (n - m) h7
Proof state after:
case inr.inr.intro.intro
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h4 : 1 < n
k : ℕ
h2 : NatPredicate N (k + 1).fib n
h3 : (k + 1).fib ≤ n
h6 : (k + 1).fib < n
h7 : NatPredicate N (n - (k + 1).fib) (k + 1).fib
hnm : n - (k + 1).fib = k.fib
⊢ ∃ k_1, (k + 1).fib = k_1.fib ∧ n = (k_1 + 1).fib
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
case inr.inr.intro.intro
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h4 : 1 < n
k : ℕ
h2 : NatPredicate N (k + 1).fib n
h3 : (k + 1).fib ≤ n
h6 : (k + 1).fib < n
h7 : NatPredicate N (n - (k + 1).fib) (k + 1).fib
hnm : n - (k + 1).fib = k.fib
⊢ ∃ k_1, (k + 1).fib = k_1.fib ∧ n = (k_1 + 1).fib
Tactic:
use k + 1, rfl
Proof state after:
case right
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h4 : 1 < n
k : ℕ
h2 : NatPredicate N (k + 1).fib n
h3 : (k + 1).fib ≤ n
h6 : (k + 1).fib < n
h7 : NatPredicate N (n - (k + 1).fib) (k + 1).fib
hnm : n - (k + 1).fib = k.fib
⊢ n = (k + 1 + 1).fib
Theorem: Imo1981P3.NatPredicate.imp_fib
Proof state before:
case right
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h4 : 1 < n
k : ℕ
h2 : NatPredicate N (k + 1).fib n
h3 : (k + 1).fib ≤ n
h6 : (k + 1).fib < n
h7 : NatPredicate N (n - (k + 1).fib) (k + 1).fib
hnm : n - (k + 1).fib = k.fib
⊢ n = (k + 1 + 1).fib
Tactic:
rw [fib_add_two, ← hnm, tsub_add_cancel_of_le h3]
Proof state after:
no goals
Theorem: Imo1981P3.m_n_bounds
Proof state before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Tactic:
obtain ⟨k : ℕ, hm : m = fib k, hn : n = fib (k + 1)⟩ := h1.imp_fib m
Proof state after:
case intro.intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Theorem: Imo1981P3.m_n_bounds
Proof state before:
case intro.intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Tactic:
by_cases h2 : k < K + 1
Proof state after:
case pos
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib

case neg
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Theorem: Imo1981P3.m_n_bounds
Proof state before:
case pos
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Tactic:
have h3 : k ≤ K := Nat.lt_succ_iff.mp h2
Proof state after:
case pos
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
h3 : k ≤ K
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Theorem: Imo1981P3.m_n_bounds
Proof state before:
case pos
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
h3 : k ≤ K
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Tactic:
constructor
Proof state after:
case pos.left
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
h3 : k ≤ K
⊢ m ≤ K.fib

case pos.right
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
h3 : k ≤ K
⊢ n ≤ (K + 1).fib
Theorem: Imo1981P3.m_n_bounds
Proof state before:
case pos.left
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
h3 : k ≤ K
⊢ m ≤ K.fib
Tactic:
calc
  m = fib k := hm
  _ ≤ fib K := fib_mono h3
Proof state after:
no goals
Theorem: Imo1981P3.m_n_bounds
Proof state before:
case pos.right
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
h3 : k ≤ K
⊢ n ≤ (K + 1).fib
Tactic:
have h6 : k + 1 ≤ K + 1 := succ_le_succ h3
Proof state after:
case pos.right
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
h3 : k ≤ K
h6 : k + 1 ≤ K + 1
⊢ n ≤ (K + 1).fib
Theorem: Imo1981P3.m_n_bounds
Proof state before:
case pos.right
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
h3 : k ≤ K
h6 : k + 1 ≤ K + 1
⊢ n ≤ (K + 1).fib
Tactic:
calc
  n = fib (k + 1) := hn
  _ ≤ fib (K + 1) := fib_mono h6
Proof state after:
no goals
Theorem: Imo1981P3.m_n_bounds
Proof state before:
case neg
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Tactic:
have h7 : N < n := by
  have h8 : K + 2 ≤ k + 1 := succ_le_succ (not_lt.mp h2)
  rw [← fib_add_two] at HK
  calc
    N < fib (K + 2) := HK
    _ ≤ fib (k + 1) := (fib_mono h8)
    _ = n := hn.symm
Proof state after:
case neg
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
h7 : N < n
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Theorem: Imo1981P3.m_n_bounds
Proof state before:
case neg
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
h7 : N < n
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Tactic:
have h9 : n ≤ N := h1.n_le_N
Proof state after:
case neg
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
h7 : N < n
h9 : n ≤ N
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Theorem: Imo1981P3.m_n_bounds
Proof state before:
case neg
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
h7 : N < n
h9 : n ≤ N
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
Tactic:
exact absurd h7 h9.not_lt
Proof state after:
no goals
Theorem: Imo1981P3.m_n_bounds
Proof state before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
⊢ N < n
Tactic:
have h8 : K + 2 ≤ k + 1 := succ_le_succ (not_lt.mp h2)
Proof state after:
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
h8 : K + 2 ≤ k + 1
⊢ N < n
Theorem: Imo1981P3.m_n_bounds
Proof state before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
h8 : K + 2 ≤ k + 1
⊢ N < n
Tactic:
rw [← fib_add_two] at HK
Proof state after:
N K : ℕ
HK : N < (K + 2).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
h8 : K + 2 ≤ k + 1
⊢ N < n
Theorem: Imo1981P3.m_n_bounds
Proof state before:
N K : ℕ
HK : N < (K + 2).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : ¬k < K + 1
h8 : K + 2 ≤ k + 1
⊢ N < n
Tactic:
calc
  N < fib (K + 2) := HK
  _ ≤ fib (k + 1) := (fib_mono h8)
  _ = n := hn.symm
Proof state after:
no goals
Theorem: Imo1981P3.k_bound
Proof state before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N m n
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
have h2 : 0 ≤ m := h1.m_range.left.le
Proof state after:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 0 ≤ m
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Theorem: Imo1981P3.k_bound
Proof state before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 0 ≤ m
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
have h3 : 0 ≤ n := h1.n_range.left.le
Proof state after:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 0 ≤ m
h3 : 0 ≤ n
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Theorem: Imo1981P3.k_bound
Proof state before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 0 ≤ m
h3 : 0 ≤ n
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
rw [← natAbs_of_nonneg h2, ← natAbs_of_nonneg h3] at h1
Proof state after:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h2 : 0 ≤ m
h3 : 0 ≤ n
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Theorem: Imo1981P3.k_bound
Proof state before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h2 : 0 ≤ m
h3 : 0 ≤ n
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
clear h2 h3
Proof state after:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Theorem: Imo1981P3.k_bound
Proof state before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
obtain ⟨h4 : m.natAbs ≤ fib K, h5 : n.natAbs ≤ fib (K + 1)⟩ := m_n_bounds HK h1
Proof state after:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Theorem: Imo1981P3.k_bound
Proof state before:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
have h6 : m ^ 2 ≤ (fib K : ℤ) ^ 2 := Int.natAbs_le_iff_sq_le.mp h4
Proof state after:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
h6 : m ^ 2 ≤ ↑K.fib ^ 2
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Theorem: Imo1981P3.k_bound
Proof state before:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
h6 : m ^ 2 ≤ ↑K.fib ^ 2
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
have h7 : n ^ 2 ≤ (fib (K + 1) : ℤ) ^ 2 := Int.natAbs_le_iff_sq_le.mp h5
Proof state after:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
h6 : m ^ 2 ≤ ↑K.fib ^ 2
h7 : n ^ 2 ≤ ↑(K + 1).fib ^ 2
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Theorem: Imo1981P3.k_bound
Proof state before:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
h6 : m ^ 2 ≤ ↑K.fib ^ 2
h7 : n ^ 2 ≤ ↑(K + 1).fib ^ 2
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1981P3.solution_greatest
Proof state before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
H : ProblemPredicate N ↑K.fib ↑(K + 1).fib
⊢ ↑M = ↑K.fib ^ 2 + ↑(K + 1).fib ^ 2
Tactic:
simp [HM]
Proof state after:
no goals
Theorem: Usa1985P1.nicomachus
Proof state before:
n : ℕ
⊢ ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
Tactic:
induction' n with n ih
Proof state after:
case zero

⊢ ∑ i ∈ Finset.range 0, i ^ 3 = (∑ i ∈ Finset.range 0, i) ^ 2

case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
⊢ ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
Theorem: Usa1985P1.nicomachus
Proof state before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
⊢ ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
Tactic:
rw [Finset.sum_range_succ, ih, Finset.sum_range_succ]
Proof state after:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x + n) ^ 2
Theorem: Usa1985P1.nicomachus
Proof state before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x + n) ^ 2
Tactic:
have h1 : ((∑ x ∈ Finset.range n, x) + n) ^ 2 =
    ((∑ x ∈ Finset.range n, x))^2 +
       (2 * (∑ x ∈ Finset.range n, x) * n +
         n ^ 2) := by ring
Proof state after:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x + n) ^ 2
Theorem: Usa1985P1.nicomachus
Proof state before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x + n) ^ 2
Tactic:
rw [h1]
Proof state after:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
Theorem: Usa1985P1.nicomachus
Proof state before:
case succ
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h2 : n ^ 3 = (2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2
⊢ (∑ i ∈ Finset.range n, i) ^ 2 + n ^ 3 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
Tactic:
omega
Proof state after:
no goals
Theorem: Usa1985P1.nicomachus
Proof state before:
case zero

⊢ ∑ i ∈ Finset.range 0, i ^ 3 = (∑ i ∈ Finset.range 0, i) ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1985P1.nicomachus
Proof state before:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
⊢ (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
Tactic:
ring
Proof state after:
no goals
Theorem: Usa1985P1.nicomachus
Proof state before:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
⊢ n ^ 3 = (2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2
Tactic:
have h5 : 2 * ∑ x ∈ Finset.range n, x =
           (∑ x ∈ Finset.range n, x) * 2 := mul_comm _ _
Proof state after:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h5 : 2 * ∑ x ∈ Finset.range n, x = (∑ x ∈ Finset.range n, x) * 2
⊢ n ^ 3 = (2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2
Theorem: Usa1985P1.nicomachus
Proof state before:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h5 : 2 * ∑ x ∈ Finset.range n, x = (∑ x ∈ Finset.range n, x) * 2
⊢ n ^ 3 = (2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2
Tactic:
rw [h5, Finset.sum_range_id_mul_two]
Proof state after:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h5 : 2 * ∑ x ∈ Finset.range n, x = (∑ x ∈ Finset.range n, x) * 2
⊢ n ^ 3 = n * (n - 1) * n + n ^ 2
Theorem: Usa1985P1.nicomachus
Proof state before:
n : ℕ
ih : ∑ i ∈ Finset.range n, i ^ 3 = (∑ i ∈ Finset.range n, i) ^ 2
h1 : (∑ x ∈ Finset.range n, x + n) ^ 2 = (∑ x ∈ Finset.range n, x) ^ 2 + ((2 * ∑ x ∈ Finset.range n, x) * n + n ^ 2)
h5 : 2 * ∑ x ∈ Finset.range n, x = (∑ x ∈ Finset.range n, x) * 2
⊢ n ^ 3 = n * (n - 1) * n + n ^ 2
Tactic:
cases' n with n
Proof state after:
case zero
ih : ∑ i ∈ Finset.range 0, i ^ 3 = (∑ i ∈ Finset.range 0, i) ^ 2
h1 : (∑ x ∈ Finset.range 0, x + 0) ^ 2 = (∑ x ∈ Finset.range 0, x) ^ 2 + ((2 * ∑ x ∈ Finset.range 0, x) * 0 + 0 ^ 2)
h5 : 2 * ∑ x ∈ Finset.range 0, x = (∑ x ∈ Finset.range 0, x) * 2
⊢ 0 ^ 3 = 0 * (0 - 1) * 0 + 0 ^ 2

case succ
n : ℕ
ih : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
h1 :
  (∑ x ∈ Finset.range (n + 1), x + (n + 1)) ^ 2 =
    (∑ x ∈ Finset.range (n + 1), x) ^ 2 + ((2 * ∑ x ∈ Finset.range (n + 1), x) * (n + 1) + (n + 1) ^ 2)
h5 : 2 * ∑ x ∈ Finset.range (n + 1), x = (∑ x ∈ Finset.range (n + 1), x) * 2
⊢ (n + 1) ^ 3 = (n + 1) * (n + 1 - 1) * (n + 1) + (n + 1) ^ 2