theorem RealAnalysis.subseq_nat_le_subseq_iff {σ : ℕ → ℕ} {n m : ℕ} (h : Subseq σ) : σ n ≤ σ m ↔ n ≤ m

theorem RealAnalysis.tendsTo_of_eventually_subseq_cover {a : ℕ → ℝ} {s : Finset (ℕ → ℕ)} {L : ℝ} (h₁ : ∀ σ ∈ s, Subseq σ) (h₂ : eventually fun (n : ℕ) => ∃ σ ∈ s, ∃ (i : ℕ), σ i = n) (h₃ : ∀ σ ∈ s, tendsTo (fun (x : ℕ) => a (σ x)) L) : tendsTo a L