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

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

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

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

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

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

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