ProbabilityTheory.IndepFun.finsetSum

lemma IndepFun.finsetSum [m : MeasurableSpace β'] [AddCommMonoid β'] [MeasurableAdd₂ β']    {f : ι → Ω → β'} {s t : Finset ι} (hf_Indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i))    (h_disj : Disjoint s t) : IndepFun (∑ i ∈ s, f i) (∑ i ∈ t, f i) μ := by  let S : Bool → Finset ι := fun b => if b then s else t  have h_disjoint : Set.PairwiseDisjoint Set.univ S := by    intro b _ c _ hbc    by_cases hb : b    · by_cases hc : c      · exfalso; exact hbc (hb ▸ hc.symm)      · simpa [hb, hc, Function.onFun, S] using h_disj    · by_cases hc : c      · simpa [hb, hc, Function.onFun, S] using h_disj.symm      · exfalso; exact hbc (eq_false_of_ne_true hb ▸ (eq_false_of_ne_true hc).symm)  have hindep := iIndepFun.finsetSum S h_disjoint hf_Indep hf_meas  have h_true : S true = s := by simp [S]  have h_false : S false = t := by simp [S]  rw [← h_true, ← h_false]  convert hindep.indepFun Bool.true_eq_false_eq_False  all_goals simp