Theorem: squeeze (LeanTeaching/TutoLib.lean)

State before:
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
⊢ seq_limit v l
Tactic:
intros ε ε_pos
State after:
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε

State before:
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε
Tactic:
cases' hu ε ε_pos with N hN
State after:
case intro
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε

State before:
case intro
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε
Tactic:
cases' hw ε ε_pos with N' hN'
State after:
case intro.intro
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε

State before:
case intro.intro
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε
Tactic:
use max N N'
State after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
⊢ ∀ n ≥ max N N', |v n - l| ≤ ε

State before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
⊢ ∀ n ≥ max N N', |v n - l| ≤ ε
Tactic:
intros n hn
State after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ max N N'
⊢ |v n - l| ≤ ε

State before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ max N N'
⊢ |v n - l| ≤ ε
Tactic:
rw [ge_max_iff] at hn
State after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
⊢ |v n - l| ≤ ε

State before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
⊢ |v n - l| ≤ ε
Tactic:
specialize hN n (by linarith)
State after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
⊢ |v n - l| ≤ ε

State before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
⊢ |v n - l| ≤ ε
Tactic:
specialize hN' n (by linarith)
State after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
⊢ |v n - l| ≤ ε

State before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
⊢ |v n - l| ≤ ε
Tactic:
specialize h n
State after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
h : u n ≤ v n
⊢ |v n - l| ≤ ε

State before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
h : u n ≤ v n
⊢ |v n - l| ≤ ε
Tactic:
specialize h' n
State after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
h : u n ≤ v n
h' : v n ≤ w n
⊢ |v n - l| ≤ ε

State before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
h : u n ≤ v n
h' : v n ≤ w n
⊢ |v n - l| ≤ ε
Tactic:
rw [abs_le] at *
State after:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : -ε ≤ u n - l ∧ u n - l ≤ ε
hN' : -ε ≤ w n - l ∧ w n - l ≤ ε
h : u n ≤ v n
h' : v n ≤ w n
⊢ -ε ≤ v n - l ∧ v n - l ≤ ε

State before:
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : -ε ≤ u n - l ∧ u n - l ≤ ε
hN' : -ε ≤ w n - l ∧ w n - l ≤ ε
h : u n ≤ v n
h' : v n ≤ w n
⊢ -ε ≤ v n - l ∧ v n - l ≤ ε
Tactic:
constructor <;> linarith
State after:
no goals

State before:
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
⊢ n ≥ N
Tactic:
linarith
State after:
no goals

State before:
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
⊢ n ≥ N'
Tactic:
linarith
State after:
no goals