Theorem: limit_const_sub_inv_succ (LeanTeaching/TutoLib.lean)

State before:
x : ℝ
⊢ seq_limit (fun n => x - 1 / (↑n + 1)) x
Tactic:
refine limit_of_sub_le_inv_succ (fun n ↦ ?_)
State after:
x : ℝ
n : ℕ
⊢ |x - 1 / (↑n + 1) - x| ≤ 1 / (↑n + 1)

State before:
x : ℝ
n : ℕ
⊢ |x - 1 / (↑n + 1) - x| ≤ 1 / (↑n + 1)
Tactic:
rw [show x - 1 / (n + 1) - x = -(1/(n+1)) from by ring, abs_neg,  abs_of_pos]
State after:
x : ℝ
n : ℕ
⊢ 0 < 1 / (↑n + 1)

State before:
x : ℝ
n : ℕ
⊢ 0 < 1 / (↑n + 1)
Tactic:
linarith [@Nat.one_div_pos_of_nat ℝ _ n]
State after:
no goals

State before:
x : ℝ
n : ℕ
⊢ x - 1 / (↑n + 1) - x = -(1 / (↑n + 1))
Tactic:
ring
State after:
no goals