Theorem: C03S06.exists_abs_le_of_convergesTo (LeanCourse/MIL/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean)

State before:
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b
Tactic:
rcases cs 1 zero_lt_one with ⟨N, h⟩
State after:
case intro
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b

State before:
case intro
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b
Tactic:
use N, |a| + 1
State after:
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∀ (n : ℕ), N ≤ n → |s n| < |a| + 1

State before:
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∀ (n : ℕ), N ≤ n → |s n| < |a| + 1
Tactic:
intro n ngt
State after:
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ |s n| < |a| + 1

State before:
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ |s n| < |a| + 1
Tactic:
calc
  |s n| = |s n - a + a| := by
    congr
    abel
  _ ≤ |s n - a| + |a| := (abs_add _ _)
  _ < |a| + 1 := by linarith [h n ngt]
State after:
no goals

State before:
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ |s n| = |s n - a + a|
Tactic:
congr
State after:
case e_a
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ s n = s n - a + a

State before:
case e_a
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ s n = s n - a + a
Tactic:
abel
State after:
no goals

State before:
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ |s n - a| + |a| < |a| + 1
Tactic:
linarith [h n ngt]
State after:
no goals