From 'a.e. for each rational t' to 'a.e. for all real t' with a monotone sandwich

This is the pattern for an empirical-CDF statement F_N(t) = #{n<N : uₙ ≤ t}/N → L(t) holding a.e. for every real t at once, with L continuous. (1) For each rational q get ∀ᵐ x from Birkhoff, then combine them with ae_all_iff (ℚ is countable; put the range condition 0 ≤ q ≤ 1 inside as an implication and handle the out-of-range case with Eventually.of_forall + absurd). (2) Fix x and t, then rw [tendsto_order]. For a < L t: take δ from Metric.eventually_nhds_iff.1 ((hL.eventually (lt_mem_nhds ha))). Pick q ∈ (max (t-δ) 0, t) with exists_rat_btwn. Then use (tendsto_order.1 (hx q ..)).1 a haq and monotonicity F_N q ≤ F_N t. The upper bound is symmetric with gt_mem_nhds and min (t+δ) 1. Endpoints (t = 0 or 1) need a separate trivial case because no rational exists on the needed side; use 0 ≤ F ≤ 1. Monotonicity of the filter card in t is just gcongr, which closes card (filter (· ≤ s)) ≤ card (filter (· ≤ t)) on its own.