Theorem: Section2sheet3.tendsTo_const (FormalisingMathematics2024/Section02reals/Sheet3.lean)

State before:
c : ℝ
⊢ TendsTo (fun n => c) c
Tactic:
intro ε hε
State after:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c) n - c| < ε

State before:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c) n - c| < ε
Tactic:
dsimp only
State after:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε

State before:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε
Tactic:
use 37
State after:
case h
c ε : ℝ
hε : ε > 0
⊢ ∀ (n : ℕ), 37 ≤ n → |c - c| < ε

State before:
case h
c ε : ℝ
hε : ε > 0
⊢ ∀ (n : ℕ), 37 ≤ n → |c - c| < ε
Tactic:
intro n hn
State after:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |c - c| < ε

State before:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |c - c| < ε
Tactic:
ring_nf
State after:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |0| < ε

State before:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |0| < ε
Tactic:
norm_num
State after:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ 0 < ε

State before:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ 0 < ε
Tactic:
exact hε
State after:
no goals