Theorem: inv_succ_le_all (LeanTeaching/TutoLib.lean)

State before:
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
Tactic:
intro ε hε
State after:
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε

State before:
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
Tactic:
obtain ⟨N, hN⟩ := Metric.tendsto_atTop.1 tendsto_one_div_add_atTop_nhds_0_nat (ε/2) (by linarith)
State after:
case intro
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε

State before:
case intro
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
Tactic:
refine ⟨N, fun n hn ↦ ?_⟩
State after:
case intro
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 1 / (↑n + 1) ≤ ε

State before:
case intro
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 1 / (↑n + 1) ≤ ε
Tactic:
convert (lt_trans (hN n hn) (half_lt_self hε)).le using 1
State after:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 1 / (↑n + 1) = dist (1 / (↑n + 1)) 0

State before:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 1 / (↑n + 1) = dist (1 / (↑n + 1)) 0
Tactic:
simp only [one_div, Real.dist_eq, sub_zero]
State after:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ (↑n + 1)⁻¹ = |(↑n + 1)⁻¹|

State before:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ (↑n + 1)⁻¹ = |(↑n + 1)⁻¹|
Tactic:
rw [abs_of_nonneg]
State after:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 0 ≤ (↑n + 1)⁻¹

State before:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 0 ≤ (↑n + 1)⁻¹
Tactic:
simp only [inv_nonneg]
State after:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 0 ≤ ↑n + 1

State before:
case h.e'_3
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
n : ℕ
hn : n ≥ N
⊢ 0 ≤ ↑n + 1
Tactic:
linarith
State after:
no goals

State before:
ε : ℝ
hε : ε > 0
⊢ ε / 2 > 0
Tactic:
linarith
State after:
no goals