Theorem: cluster_limit (GlimpseOfLean/Solutions/Topics/SequenceLimits.lean)

State before:
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
ha : cluster_point u a
⊢ a = l
Tactic:
rcases ha with ⟨φ, φ_extr, lim_u_φ⟩
State after:
case intro.intro
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
φ : ℕ → ℕ
φ_extr : extraction φ
lim_u_φ : seq_limit (u ∘ φ) a
⊢ a = l

State before:
case intro.intro
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
φ : ℕ → ℕ
φ_extr : extraction φ
lim_u_φ : seq_limit (u ∘ φ) a
⊢ a = l
Tactic:
have lim_u_φ' : seq_limit (u ∘ φ) l := subseq_tendsto_of_tendsto' hl φ_extr
State after:
case intro.intro
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
φ : ℕ → ℕ
φ_extr : extraction φ
lim_u_φ : seq_limit (u ∘ φ) a
lim_u_φ' : seq_limit (u ∘ φ) l
⊢ a = l

State before:
case intro.intro
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
φ : ℕ → ℕ
φ_extr : extraction φ
lim_u_φ : seq_limit (u ∘ φ) a
lim_u_φ' : seq_limit (u ∘ φ) l
⊢ a = l
Tactic:
exact unique_limit lim_u_φ lim_u_φ'
State after:
no goals