Theorem: Imo1981P3.NatPredicate.imp_fib (Compfiles/Imo1981P3.lean)

State before:
N n : ℕ
⊢ ∀ (m : ℕ), NatPredicate N m n → ∃ k, m = k.fib ∧ n = (k + 1).fib
Tactic:
refine Nat.strong_induction_on n ?_
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

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
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

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
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

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
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

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
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

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
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

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)
State after:
no goals

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
State after:
no goals

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
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

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)
State after:
no goals

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
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

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
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

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
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

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]
State after:
no goals