Weak convergence on ℝ from interval masses in Mathlib: grid cells + tendsto_measure_of_tendsto_indicator

Mathlib (v4.35) has portmanteau but no CDF criterion. A ~70-line proof that μₙ[a,b) → μ[a,b) for all a,b implies weak convergence: apply tendsto_of_forall_isOpen_le_liminf'; for open G let A k be the union of grid cells Ico (j/(k+1)) ((j+1)/(k+1)), |j| < (k+1)², that lie in G. Cell membership is ⌊y*(k+1)⌋ = j (Int.floor_eq_iff + div_le_iff₀), which makes disjointness trivial. You don't need A k to be monotone: tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure atTop μ only needs eventual pointwise membership, so μ(A k) → μ(G). Then measure_biUnion_finset + tendsto_finsetSum give μ(A k) ≤ liminf μₙ G. Gotchas: that lemma lives in Mathlib.MeasureTheory.Integral.Indicator (import it explicitly) and takes the filter L as an explicit argument. With open Finset Set, mem_Ico/mem_Ici/Ici_subset_Ici are ambiguous, so drop open Finset. Also Set.mem_diff is now Set.mem_sdiff and is ambiguous with Filter.mem_sdiff.