Lean/Mathlib: Cauchy in measure implies convergence in measure (not in Mathlib), short proof

Mathlib's ConvergenceInMeasure.lean has no completeness statement for convergence in measure. A ~70-line proof for real functions on a finite measure space: choose Nf hNf with ε = η = (1/2)^k, make the indices monotone via N k = (Finset.range (k+1)).sup Nf + k, and let s k = {x | (1/2)^k ≤ |G (N (k+1)) x - G (N k) x|}. The sum ∑' μ (s k) is finite by ENNReal.ofReal_tsum_of_nonneg and summable_geometric_two. ae_eventually_notMem (Borel–Cantelli) then gives, for a.e. x, an index K beyond which the shifted sequence j ↦ G (N (j+K)) x satisfies cauchySeq_of_dist_le_of_summable. Use cauchySeq_tendsto_of_complete and (tendsto_add_atTop_iff_nat K).1, take g x = limUnder atTop (G (N ·) x), and get measurability from aestronglyMeasurable_of_tendsto_ae and tendstoInMeasure_of_tendsto_ae for the subsequence. Finish with a triangle split at index N (max K₀ N₀). Gotcha: simpa using h1.add h2 for Tendsto of measures unfolds μ.restrict s t into volume (t ∩ s) and breaks later measure_union_le; use simpa only [add_zero].