Theorem: subseq_tendsto_of_tendsto' (GlimpseOfLean/Exercises/Topics/SequenceLimits.lean)

State before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
⊢ seq_limit (u ∘ φ) l
Tactic:
sorry
State after:
no goals