Theorem: tends_to_const (FM2023Exrcise/section02_reals/sheet3.lean)

State before:
c : ℝ
⊢ tends_to (fun x => c) c
Tactic:
rw [tends_to_def]
State after:
c : ℝ
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε

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

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

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

State before:
case h
c ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ |c - c| < ε
Tactic:
norm_num
State after:
case h
c ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ 0 < ε

State before:
case h
c ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ 0 < ε
Tactic:
apply hε
State after:
no goals