Theorem: exercise2_8 (LeanCourse/Assignments/Assignment2.lean)

State before:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
⊢ ∀ (k : ℕ), ∃ N, ∀ n ≥ N, s n ≥ k
Tactic:
have h3s : ∀ n, 1 ≤ s n := by
  intro n
  exact?
State after:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
⊢ ∀ (k : ℕ), ∃ N, ∀ n ≥ N, s n ≥ k

State before:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
⊢ ∀ (k : ℕ), ∃ N, ∀ n ≥ N, s n ≥ k
Tactic:
sorry
State after:
no goals

State before:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
⊢ ∀ (n : ℕ), 1 ≤ s n
Tactic:
intro n
State after:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
n : ℕ
⊢ 1 ≤ s n

State before:
s t : ℕ → ℕ
k : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
n : ℕ
⊢ 1 ≤ s n
Tactic:
exact?
State after:
no goals