Theorem: exercise3_3 (LeanCourse/Assignments/Solutions/Solutions3.lean)

State before:
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
⊢ SequentialLimit (s ∘ r) a
Tactic:
intro ε hε
State after:
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε

State before:
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε
Tactic:
obtain ⟨N, hN⟩ := hs ε hε
State after:
case intro
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε

State before:
case intro
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε
Tactic:
obtain ⟨K, hK⟩ := hr N
State after:
case intro.intro
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε

State before:
case intro.intro
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε
Tactic:
use K
State after:
case h
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
⊢ ∀ n ≥ K, |(s ∘ r) n - a| < ε

State before:
case h
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
⊢ ∀ n ≥ K, |(s ∘ r) n - a| < ε
Tactic:
intro n hn
State after:
case h
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ |(s ∘ r) n - a| < ε

State before:
case h
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ |(s ∘ r) n - a| < ε
Tactic:
apply hN
State after:
case h.a
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ r n ≥ N

State before:
case h.a
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ r n ≥ N
Tactic:
apply hK
State after:
case h.a.a
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ n ≥ K

State before:
case h.a.a
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ n ≥ K
Tactic:
assumption
State after:
no goals