Theorem: exercise3_6 (LeanCourse/Assignments/Solutions/Solutions3.lean)

State before:
⊢ SequentialLimit (fun n => sin ↑n / (↑n + 1)) 0
Tactic:
apply exercise3_4 use_me exercise3_5
State after:
case hs₁s₂

⊢ ∀ (n : ℕ), -1 / (↑n + 1) ≤ sin ↑n / (↑n + 1)

case hs₂s₃

⊢ ∀ (n : ℕ), sin ↑n / (↑n + 1) ≤ 1 / (↑n + 1)

State before:
case hs₁s₂

⊢ ∀ (n : ℕ), -1 / (↑n + 1) ≤ sin ↑n / (↑n + 1)
Tactic:
intro n
State after:
case hs₁s₂
n : ℕ
⊢ -1 / (↑n + 1) ≤ sin ↑n / (↑n + 1)

State before:
case hs₁s₂
n : ℕ
⊢ -1 / (↑n + 1) ≤ sin ↑n / (↑n + 1)
Tactic:
gcongr
State after:
case hs₁s₂.h
n : ℕ
⊢ -1 ≤ sin ↑n

State before:
case hs₁s₂.h
n : ℕ
⊢ -1 ≤ sin ↑n
Tactic:
apply?
State after:
no goals

State before:
case hs₂s₃

⊢ ∀ (n : ℕ), sin ↑n / (↑n + 1) ≤ 1 / (↑n + 1)
Tactic:
intro n
State after:
case hs₂s₃
n : ℕ
⊢ sin ↑n / (↑n + 1) ≤ 1 / (↑n + 1)

State before:
case hs₂s₃
n : ℕ
⊢ sin ↑n / (↑n + 1) ≤ 1 / (↑n + 1)
Tactic:
gcongr
State after:
case hs₂s₃.h
n : ℕ
⊢ sin ↑n ≤ 1

State before:
case hs₂s₃.h
n : ℕ
⊢ sin ↑n ≤ 1
Tactic:
apply?
State after:
no goals