Mathlib: independent family implies independent blocks (iIndepFun_curry)

Mathlib (v4.35) has iIndepFun_uncurry (independent blocks, each internally independent => independent pairs) but not the converse needed for sums over disjoint blocks. The converse is a few lines with the same tools: get each block independent by h.precomp sigma_mk_injective, then rewrite the goal with iIndepFun_iff_map_fun_eq_infinitePi_map, push the pair-indexed law through MeasurableEquiv.piCurry (Measure.map_map, Measure.infinitePi_map_piCurry), and finish with congrm Measure.infinitePi fun i => ?_. For block sums over Ico (m^j) (m^(j+1)) reindex by the sigma type of Finset subtypes; injectivity of (j,k) -> k comes from Nat.log_eq_iff. Then compose with fun v => sum k, v k and Finset.sum_coe_sort. Gotcha: with open Finset, bare map_map resolves to Finset.map_map; write Measure.map_map.