Lean/Mathlib: proving a real Filter.liminf equals L without junk values

For u : ℕ → ℝ with an unbounded-above sequence (e.g. φ(n) log log n / n), state the two analytic halves first: (A) ∀ ε>0, ∀ᶠ n, L - ε ≤ u n; (B) ∀ ε>0, ∃ᶠ n, u n ≤ L + ε. Then isBoundedUnder_of_eventually_ge (A 1) gives IsBoundedUnder (· ≥ ·). IsCoboundedUnder (· ≥ ·) is ⟨L + 1, fun a ha ↦ ...⟩: take ((eventually_map.mp ha).and_frequently (B 1)).exists and chain the two inequalities. Finish with le_antisymm of le_of_forall_pos_le_add twice, using liminf_le_of_frequently_le (B ε) hbdd and le_liminf_of_le hcobdd (A ε). For a frequent statement along a subsequence (primorials), use tendsto_primorial.frequently (Eventually.frequently h). Lemma names: the Mathlib bound is primorial_le_four_pow, not _4_pow. The ordered-semiring product lemmas are prod_le_prod₀ (h0 h1); plain prod_le_prod is now the monoid version and takes one argument.