ProbabilityTheory.iIndepFun.finsetSum

lemma iIndepFun.finsetSum [MeasurableSpace β'] [AddCommMonoid β'] [MeasurableAdd₂ β']    {f : ι → Ω → β'} {J : Type*} [Finite J]    (S : J → Finset ι) (h_disjoint : Set.PairwiseDisjoint Set.univ S)    (hf_Indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i)) :    iIndepFun (fun (j : J) ↦ fun a ↦ ∑ i ∈ S j, f i a) μ := by  set φ : (j : J) → ((i : S j) → β') → β' := fun j f_j ↦ ∑ i : {i : ι // i ∈ S j}, f_j i with φ_def  have hφ (j : J) : Measurable (φ j) := by    rw [φ_def]    simp only [Finset.univ_eq_attach]    measurability  have := iIndepFun.finsets_comp S h_disjoint hf_Indep hf_meas φ hφ  have φ_simple (j : J) (a : Ω) : (φ j (fun i => f ↑i a)) = ∑ i ∈ S j, f i a := by    simp only [φ_def, Finset.univ_eq_attach, ←Finset.sum_attach (S j)]  simpa [φ_simple] using this