Theorem: Tutorial.nestedIntervalSeq_tendsto (Solution/Advanced/Analysis/Lecture3.lean)

State before:
ι : Type
U : ι → Set ℝ
⊢ Tendsto (nestedIntervalSeq U) atTop (𝓝 (CauSeq.lim (nestedIntervalCauSeq U)))
Tactic:
apply (nestedIntervalCauSeq U).tendsto_limit
State after:
no goals