Theorem: exercise3_2 (LeanCourse/Assignments/Assignment3.lean)

State before:
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
⊢ SequentialLimit (s ∘ r) a
Tactic:
sorry
State after:
no goals