Theorem: id_le_extraction' (GlimpseOfLean/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 φ
⊢ 0 ≤ φ 0
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
case succ
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
ih : n ≤ φ n
⊢ n + 1 ≤ φ (n + 1)
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 < φ (n + 1)
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