Theorem: id_le_extraction' (LCTutorial/Exercises/Topics/SequenceLimits.lean)

State before:
φ : ℕ → ℕ
⊢ extraction φ → ∀ (n : ℕ), n ≤ φ n
Tactic:
intros hyp n
State after:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
⊢ n ≤ φ n

State before:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
⊢ n ≤ φ n
Tactic:
induction n with
| zero =>  exact Nat.zero_le _
| succ n ih => exact Nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)])
State after:
no goals

State before:
case zero
φ : ℕ → ℕ
hyp : extraction φ
⊢ Nat.zero ≤ φ Nat.zero
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
case succ
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
ih : n ≤ φ n
⊢ Nat.succ n ≤ φ (Nat.succ n)
Tactic:
exact Nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)])
State after:
no goals

State before:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
ih : n ≤ φ n
⊢ n < φ (Nat.succ n)
Tactic:
linarith [hyp n (n+1) (by linarith)]
State after:
no goals

State before:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
ih : n ≤ φ n
⊢ n < n + 1
Tactic:
linarith
State after:
no goals