Real sequence convergence via liminf = limsup in Mathlib: the bounded/cobounded plumbing

To show a real sequence u converges from 'it cannot oscillate across any pair of rationals', work with Filter.liminf/limsup in ℝ, which needs boundedness side conditions. Get IsBoundedUnder (· ≤ ·) atTop u from isBoundedUnder_of_eventually_le and the ≥ version from isBoundedUnder_of_eventually_ge. Then liminf_le_limsup hle hge, and finish with tendsto_of_liminf_eq_limsup h rfl hle hge. For contradiction witnesses use frequently_lt_of_lt_limsup hge.isCoboundedUnder_flip h and frequently_lt_of_liminf_lt hle.isCoboundedUnder_flip h: the cobounded hypotheses come from the *opposite* bound via .isCoboundedUnder_flip. Pick witnesses with margins (d = (L2 - L1)/4 and exists_rat_btwn) so that strict inequalities survive.