internlm/Lean-Github huggingface dataset:
Theorem: tends_to_thirtyseven
Proof state before:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ 0 < ε
Tactic:
apply hε
Proof state after:
no goals
Theorem: tends_to_const
Proof state before:
c : ℝ
⊢ tends_to (fun x => c) c
Tactic:
rw [tends_to_def]
Proof state after:
c : ℝ
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε
Theorem: tends_to_const
Proof state before:
c : ℝ
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε
Tactic:
intro ε hε
Proof state after:
c ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε
Theorem: tends_to_const
Proof state before:
c ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε
Tactic:
use 0
Proof state after:
case h
c ε : ℝ
hε : 0 < ε
⊢ ∀ (n : ℕ), 0 ≤ n → |c - c| < ε
Theorem: tends_to_const
Proof state before:
case h
c ε : ℝ
hε : 0 < ε
⊢ ∀ (n : ℕ), 0 ≤ n → |c - c| < ε
Tactic:
intro n _
Proof state after:
case h
c ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ |c - c| < ε
Theorem: tends_to_const
Proof state before:
case h
c ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ |c - c| < ε
Tactic:
norm_num
Proof state after:
case h
c ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ 0 < ε
Theorem: tends_to_const
Proof state before:
case h
c ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ 0 < ε
Tactic:
apply hε
Proof state after:
no goals
Theorem: tends_to_add_const
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : tends_to a t
⊢ tends_to (fun n => a n + c) (t + c)
Tactic:
rw [tends_to_def] at *
Proof state after:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Theorem: tends_to_add_const
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Tactic:
intro ε hε
Proof state after:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Theorem: tends_to_add_const
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Tactic:
have hε' := h ε $ hε
Proof state after:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
hε' : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Theorem: tends_to_add_const
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
hε' : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Tactic:
obtain ⟨B', hε''⟩ := hε'
Proof state after:
case intro
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Theorem: tends_to_add_const
Proof state before:
case intro
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Tactic:
use B'
Proof state after:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
⊢ ∀ (n : ℕ), B' ≤ n → |a n + c - (t + c)| < ε
Theorem: tends_to_add_const
Proof state before:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
⊢ ∀ (n : ℕ), B' ≤ n → |a n + c - (t + c)| < ε
Tactic:
intro n hn
Proof state after:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
⊢ |a n + c - (t + c)| < ε
Theorem: tends_to_add_const
Proof state before:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
⊢ |a n + c - (t + c)| < ε
Tactic:
have h' := hε'' n hn
Proof state after:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
h' : |a n - t| < ε
⊢ |a n + c - (t + c)| < ε
Theorem: tends_to_add_const
Proof state before:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
h' : |a n - t| < ε
⊢ |a n + c - (t + c)| < ε
Tactic:
norm_num
Proof state after:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
h' : |a n - t| < ε
⊢ |a n - t| < ε
Theorem: tends_to_add_const
Proof state before:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
h' : |a n - t| < ε
⊢ |a n - t| < ε
Tactic:
apply h'
Proof state after:
no goals
Theorem: tends_to_neg
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : tends_to a t
⊢ tends_to (fun n => -a n) (-t)
Tactic:
rw [tends_to_def] at *
Proof state after:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Theorem: tends_to_neg
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Tactic:
intro ε hεpos
Proof state after:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Theorem: tends_to_neg
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Tactic:
obtain ⟨N, h⟩ := ha ε hεpos
Proof state after:
case intro
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Theorem: tends_to_neg
Proof state before:
case intro
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Tactic:
use N
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
⊢ ∀ (n : ℕ), N ≤ n → |-a n - -t| < ε
Theorem: tends_to_neg
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
⊢ ∀ (n : ℕ), N ≤ n → |-a n - -t| < ε
Tactic:
intro n hn
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
⊢ |-a n - -t| < ε
Theorem: tends_to_neg
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
⊢ |-a n - -t| < ε
Tactic:
simp
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
⊢ |-a n + t| < ε
Theorem: tends_to_neg
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
⊢ |-a n + t| < ε
Tactic:
have h' := h n hn
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |a n - t| < ε
⊢ |-a n + t| < ε
Theorem: tends_to_neg
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |a n - t| < ε
⊢ |-a n + t| < ε
Tactic:
rw [← abs_neg] at h'
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |(-(a n - t))| < ε
⊢ |-a n + t| < ε
Theorem: tends_to_neg
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |(-(a n - t))| < ε
⊢ |-a n + t| < ε
Tactic:
simp at h'
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |t - a n| < ε
⊢ |-a n + t| < ε
Theorem: tends_to_neg
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |t - a n| < ε
⊢ |-a n + t| < ε
Tactic:
rw [add_comm]
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |t - a n| < ε
⊢ |t + -a n| < ε
Theorem: tends_to_neg
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |t - a n| < ε
⊢ |t + -a n| < ε
Tactic:
apply h'
Proof state after:
no goals
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
⊢ tends_to (fun n => a n + b n) (t + u)
Tactic:
rw [tends_to_def]
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
intro ε hεpos
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
rw [tends_to] at ha
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
have haε : 0 < ε / 2 :=
  by
  linarith
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
haε : 0 < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
haε : 0 < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
apply ha at haε
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
haε : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
haε : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
obtain ⟨Na, ha'⟩ := haε
Proof state after:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
have hbε : 0 < ε / 2 :=
  by
  linarith
Proof state after:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
hbε : 0 < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
hbε : 0 < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
apply hb at hbε
Proof state after:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
hbε : ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
hbε : ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
obtain ⟨Nb, hb'⟩ := hbε
Proof state after:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
let Nab := max Na Nb
Proof state after:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
use Nab
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
⊢ ∀ (n : ℕ), Nab ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
⊢ ∀ (n : ℕ), Nab ≤ n → |a n + b n - (t + u)| < ε
Tactic:
intro n
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
⊢ Nab ≤ n → |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
⊢ Nab ≤ n → |a n + b n - (t + u)| < ε
Tactic:
intro hn
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
⊢ |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
have ha'' := ha' n
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
have hb'' := hb' n
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
have hNan : Na ≤ n :=
  by
  exact le_of_max_le_left hn
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : Na ≤ n
⊢ |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : Na ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
have hNbn : Nb ≤ n :=
  by
  exact le_of_max_le_right hn
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : Na ≤ n
hNbn : Nb ≤ n
⊢ |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : Na ≤ n
hNbn : Nb ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
apply ha'' at hNan
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNbn : Nb ≤ n
hNan : |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNbn : Nb ≤ n
hNan : |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
apply hb'' at hNbn
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Theorem: tends_to_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
calc
  |a n + b n - (t + u)|
    = |(a n - t) + (b n - u)| :=
    by
    apply congrArg
    ring
  _ ≤ |a n - t| + |b n - u|   :=
    by
    exact abs_add (a n - t) (b n - u)
  _ < ε / 2 + ε / 2           :=
    by
    exact add_lt_add hNan hNbn
  _ = ε                       :=
    by
    ring
Proof state after:
no goals
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
⊢ 0 < ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
⊢ 0 < ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
⊢ Na ≤ n
Tactic:
exact le_of_max_le_left hn
Proof state after:
no goals
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : Na ≤ n
⊢ Nb ≤ n
Tactic:
exact le_of_max_le_right hn
Proof state after:
no goals