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

State before:
s t : ℕ → ℕ
k : ℕ
⊢ ∃ s, EventuallyGrowsFaster (fun n => s (n + 1)) s ∧ ∀ (n : ℕ), s n ≠ 0
Tactic:
use fun n ↦ n ^ n
State after:
case h
s t : ℕ → ℕ
k : ℕ
⊢ (EventuallyGrowsFaster (fun n => (n + 1) ^ (n + 1)) fun n => n ^ n) ∧ ∀ (n : ℕ), n ^ n ≠ 0

State before:
case h
s t : ℕ → ℕ
k : ℕ
⊢ (EventuallyGrowsFaster (fun n => (n + 1) ^ (n + 1)) fun n => n ^ n) ∧ ∀ (n : ℕ), n ^ n ≠ 0
Tactic:
constructor
State after:
case h.left
s t : ℕ → ℕ
k : ℕ
⊢ EventuallyGrowsFaster (fun n => (n + 1) ^ (n + 1)) fun n => n ^ n

case h.right
s t : ℕ → ℕ
k : ℕ
⊢ ∀ (n : ℕ), n ^ n ≠ 0

State before:
case h.left
s t : ℕ → ℕ
k : ℕ
⊢ EventuallyGrowsFaster (fun n => (n + 1) ^ (n + 1)) fun n => n ^ n
Tactic:
intro k
State after:
case h.left
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * (fun n => n ^ n) n ≤ (fun n => (n + 1) ^ (n + 1)) n

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

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

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

State before:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * n ^ n ≤ (n + 1) ^ (n + 1)
Tactic:
calc k * n ^ n ≤ n * n ^ n := by gcongr
  _ = n ^ (n + 1) := by ring
  _ ≤ (n + 1) ^ (n + 1) := by
    gcongr
    simp
State after:
no goals

State before:
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ k * n ^ n ≤ n * n ^ n
Tactic:
gcongr
State after:
no goals

State before:
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n * n ^ n = n ^ (n + 1)
Tactic:
ring
State after:
no goals

State before:
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n ^ (n + 1) ≤ (n + 1) ^ (n + 1)
Tactic:
gcongr
State after:
case hab
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n ≤ n + 1

State before:
case hab
s t : ℕ → ℕ
k✝ k n : ℕ
hn : n ≥ k
⊢ n ≤ n + 1
Tactic:
simp
State after:
no goals

State before:
case h.right
s t : ℕ → ℕ
k : ℕ
⊢ ∀ (n : ℕ), n ^ n ≠ 0
Tactic:
intro n
State after:
case h.right
s t : ℕ → ℕ
k n : ℕ
⊢ n ^ n ≠ 0

State before:
case h.right
s t : ℕ → ℕ
k n : ℕ
⊢ n ^ n ≠ 0
Tactic:
apply pow_self_ne_zero
State after:
no goals