Theorem: exercise2_5 (LeanCourse/Assignments/Solutions/Solutions2.lean)

State before:
s t : ℕ → ℕ
k : ℕ
⊢ EventuallyGrowsFaster (fun n => n * s n) s
Tactic:
intro k
State after:
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * s n ≤ (fun n => n * s n) n

State before:
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * s n ≤ (fun n => n * s n) n
Tactic:
use k
State after:
case h
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∀ n ≥ k, k * s n ≤ (fun n => n * s n) n

State before:
case h
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∀ n ≥ k, k * s n ≤ (fun n => n * s n) n
Tactic:
intro n hnk
State after:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hnk : n ≥ k
⊢ k * s n ≤ (fun n => n * s n) n

State before:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hnk : n ≥ k
⊢ k * s n ≤ (fun n => n * s n) n
Tactic:
simp
State after:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hnk : n ≥ k
⊢ k * s n ≤ n * s n

State before:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hnk : n ≥ k
⊢ k * s n ≤ n * s n
Tactic:
gcongr
State after:
no goals