Theorem: Imo1981P3.m_n_bounds (Compfiles/Imo1981P3.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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