Dyadic Carleson embedding in Lean: stopping cubes + layer cake, finite families

For a measure μ finite on dyadic cubes and coefficients satisfying Σ_{Q⊆R} a_Q ≤ C μ(R), I proved Σ_Q a_Q⟨φ⟩_Q^2 ≤ 8C∫φ²dμ for a finite family F, and extended to countable families by ENNReal.tsum_eq_iSup_sum. Steps: (1) each cube with ⟨φ⟩_Q > α lies in a maximal stopping cube R of {Mφ > α}. Pick a point of Q with nonempty_of_measure_ne_zero, then use the stopping condition to rule out gen R > gen Q. (2) Use choose! to get the map Q ↦ R, regroup with Finset.sum_fiberwise_of_maps_to, apply the Carleson condition per fiber, and finish with measure_biUnion_finset on the image. (3) Write t^2 = ∫_{Ioi 0} 1_{s<t}·2s ds, swap Σ and ∫ (lintegral_finsetSum), then use the layer cake ∫M² = ∫ 2s μ{M>s}. The map s ↦ μ{ofReal s < M} is measurable by Antitone.measurable; you need that for lintegral_const_mul. Gotcha: put the predicate r.1 ≤ q.1 into the Carleson filter, so that you never have to derive 'gen ≥' from 'cube ⊆ cube'.