Theorem: tends_to_thirtyseven_mul (FM2023Exrcise/section02_reals/sheet6.lean)

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

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

State before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Tactic:
have hεpos' : 0 < ε / 37 :=
  by
  apply div_pos hεpos (by norm_num)
State after:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε

State before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Tactic:
have h' := h (ε / 37) hεpos'
State after:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
h' : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε

State before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
h' : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Tactic:
obtain ⟨N, hN⟩ := h'
State after:
case intro
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε

State before:
case intro
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Tactic:
use N
State after:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
⊢ ∀ (n : ℕ), N ≤ n → |37 * a n - 37 * t| < ε

State before:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
⊢ ∀ (n : ℕ), N ≤ n → |37 * a n - 37 * t| < ε
Tactic:
intro n hn
State after:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
⊢ |37 * a n - 37 * t| < ε

State before:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
⊢ |37 * a n - 37 * t| < ε
Tactic:
have h'' := hN n hn
State after:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ |37 * a n - 37 * t| < ε

State before:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ |37 * a n - 37 * t| < ε
Tactic:
rw [← mul_sub, abs_mul, abs_of_nonneg]
State after:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 37 * |a n - t| < ε

case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 0 ≤ 37

State before:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 37 * |a n - t| < ε

case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 0 ≤ 37
Tactic:
linarith
State after:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 0 ≤ 37

State before:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 0 ≤ 37
Tactic:
norm_num
State after:
no goals

State before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
⊢ 0 < ε / 37
Tactic:
apply div_pos hεpos (by norm_num)
State after:
no goals

State before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
⊢ 0 < 37
Tactic:
norm_num
State after:
no goals