Theorem: C03S06.convergesTo_const (LeanCourse/MIL/C03_Logic/S06_Sequences_and_Convergence.lean)

State before:
a : ℝ
⊢ ConvergesTo (fun x => a) a
Tactic:
intro ε εpos
State after:
a ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun x => a) n - a| < ε

State before:
a ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun x => a) n - a| < ε
Tactic:
use 0
State after:
case h
a ε : ℝ
εpos : ε > 0
⊢ ∀ n ≥ 0, |(fun x => a) n - a| < ε

State before:
case h
a ε : ℝ
εpos : ε > 0
⊢ ∀ n ≥ 0, |(fun x => a) n - a| < ε
Tactic:
intro n nge
State after:
case h
a ε : ℝ
εpos : ε > 0
n : ℕ
nge : n ≥ 0
⊢ |(fun x => a) n - a| < ε

State before:
case h
a ε : ℝ
εpos : ε > 0
n : ℕ
nge : n ≥ 0
⊢ |(fun x => a) n - a| < ε
Tactic:
rw [sub_self, abs_zero]
State after:
case h
a ε : ℝ
εpos : ε > 0
n : ℕ
nge : n ≥ 0
⊢ 0 < ε

State before:
case h
a ε : ℝ
εpos : ε > 0
n : ℕ
nge : n ≥ 0
⊢ 0 < ε
Tactic:
apply εpos
State after:
no goals