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

State before:
⊢ SequentialLimit (fun n => 1 / (↑n + 1)) 0
Tactic:
intro ε hε
State after:
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => 1 / (↑n + 1)) n - 0| < ε

State before:
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => 1 / (↑n + 1)) n - 0| < ε
Tactic:
use ⌈1 / ε⌉₊
State after:
case h
ε : ℝ
hε : ε > 0
⊢ ∀ n ≥ ⌈1 / ε⌉₊, |(fun n => 1 / (↑n + 1)) n - 0| < ε

State before:
case h
ε : ℝ
hε : ε > 0
⊢ ∀ n ≥ ⌈1 / ε⌉₊, |(fun n => 1 / (↑n + 1)) n - 0| < ε
Tactic:
intro n hn
State after:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : n ≥ ⌈1 / ε⌉₊
⊢ |(fun n => 1 / (↑n + 1)) n - 0| < ε

State before:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : n ≥ ⌈1 / ε⌉₊
⊢ |(fun n => 1 / (↑n + 1)) n - 0| < ε
Tactic:
simp at hn
State after:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ |(fun n => 1 / (↑n + 1)) n - 0| < ε

State before:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ |(fun n => 1 / (↑n + 1)) n - 0| < ε
Tactic:
simp [abs_inv]
State after:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ |↑n + 1|⁻¹ < ε

State before:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ |↑n + 1|⁻¹ < ε
Tactic:
rw [inv_lt]
State after:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ ε⁻¹ < |↑n + 1|

case h.ha
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ 0 < |↑n + 1|

case h.hb
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ 0 < ε

State before:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ ε⁻¹ < |↑n + 1|
Tactic:
have fact1 : (n : ℝ) + 1 ≤ |(n : ℝ) + 1| := by apply?
State after:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
fact1 : ↑n + 1 ≤ |↑n + 1|
⊢ ε⁻¹ < |↑n + 1|

State before:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
fact1 : ↑n + 1 ≤ |↑n + 1|
⊢ ε⁻¹ < |↑n + 1|
Tactic:
linarith
State after:
no goals

State before:
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ ↑n + 1 ≤ |↑n + 1|
Tactic:
apply?
State after:
no goals

State before:
case h.ha
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ 0 < |↑n + 1|
Tactic:
rw [abs_pos]
State after:
case h.ha
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ ↑n + 1 ≠ 0

State before:
case h.ha
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ ↑n + 1 ≠ 0
Tactic:
apply?
State after:
no goals

State before:
case h.hb
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ 0 < ε
Tactic:
assumption
State after:
no goals