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!
State after:
case h
s t : ℕ → ℕ
k : ℕ
⊢ (EventuallyGrowsFaster (fun n => (n + 1)!) fun n => n !) ∧ ∀ (n : ℕ), n ! ≠ 0

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

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

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

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

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

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

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

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

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

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

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

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

State before:
case h.right
s t : ℕ → ℕ
k n : ℕ
⊢ n ! ≠ 0
Tactic:
exact?
State after:
no goals