Theorem: exercise2_8 (LeanCourse/Assignments/Solutions/Solutions2.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:
intro k
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:
obtain ⟨N, hN⟩ := hs k
State after:
case intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ n ≥ N, k * s n ≤ (fun n => s (n + 1)) n
⊢ ∃ N, ∀ n ≥ N, s n ≥ k

State before:
case intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ n ≥ N, k * s n ≤ (fun n => s (n + 1)) n
⊢ ∃ N, ∀ n ≥ N, s n ≥ k
Tactic:
simp at hN
State after:
case intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
⊢ ∃ N, ∀ n ≥ N, s n ≥ k

State before:
case intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
⊢ ∃ N, ∀ n ≥ N, s n ≥ k
Tactic:
use N + 1
State after:
case h
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
⊢ ∀ n ≥ N + 1, s n ≥ k

State before:
case h
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
⊢ ∀ n ≥ N + 1, s n ≥ k
Tactic:
intros n hn
State after:
case h
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
n : ℕ
hn : n ≥ N + 1
⊢ s n ≥ k

State before:
case h
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
n : ℕ
hn : n ≥ N + 1
⊢ s n ≥ k
Tactic:
obtain ⟨n', hn'N, hn'n⟩ := useful_fact2 hn
State after:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
⊢ s n ≥ k

State before:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N : ℕ
hN : ∀ (n : ℕ), N ≤ n → k * s n ≤ s (n + 1)
n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
⊢ s n ≥ k
Tactic:
specialize hN n' hn'N
State after:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s (n' + 1)
⊢ s n ≥ k

State before:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s (n' + 1)
⊢ s n ≥ k
Tactic:
rw [hn'n] at hN
State after:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ s n ≥ k

State before:
case h.intro.intro
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ s n ≥ k
Tactic:
calc k = k * 1 := by simp
  _ ≤ k * s n' := by
    gcongr
    apply h3s
  _ ≤ s n := by assumption
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

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 : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ k = k * 1
Tactic:
simp
State after:
no goals

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 : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ k * 1 ≤ k * s n'
Tactic:
gcongr
State after:
case bc
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ 1 ≤ s n'

State before:
case bc
s t : ℕ → ℕ
k✝ : ℕ
hs : EventuallyGrowsFaster (fun n => s (n + 1)) s
h2s : ∀ (n : ℕ), s n ≠ 0
h3s : ∀ (n : ℕ), 1 ≤ s n
k N n : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ 1 ≤ s n'
Tactic:
apply h3s
State after:
no goals

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 : ℕ
hn : n ≥ N + 1
n' : ℕ
hn'N : n' ≥ N
hn'n : n' + 1 = n
hN : k * s n' ≤ s n
⊢ k * s n' ≤ s n
Tactic:
assumption
State after:
no goals