ProbabilityTheory.iIndepFun.sum_elim

lemma ProbabilityTheory.iIndepFun.sum_elim {Ω I J G : Type*} [MeasurableSpace Ω] [MeasurableSpace G]    (μ : Measure Ω) {f : I → Ω → G} {g : J → Ω → G} (hf_indep : iIndepFun f μ)    (hg_indep : iIndepFun g μ) (hindep : IndepFun (fun ω x ↦ f x ω) (fun ω y ↦ g y ω) μ) :    iIndepFun (Sum.elim f g) μ := by  rw [iIndepFun_iff] at hf_indep hg_indep ⊢  intro s E hE  have : s.toLeft.disjSum s.toRight = s := Finset.toLeft_disjSum_toRight  rw [←this, Finset.prod_disjSum,←hf_indep,←hg_indep]  · simp_rw [MeasurableSpace.measurableSet_comap] at hE    choose F hF using hE    let S := ⋂ (i :s.toLeft), {x: I → G | x i ∈ F (Sum.inl i) (Finset.mem_toLeft.mp i.property)}    let T := ⋂ (j:s.toRight), {y: J → G | y j ∈ F (Sum.inr j) (Finset.mem_toRight.mp j.property)}    convert hindep.measure_inter_preimage_eq_mul S T _ _    · ext ω      simp only [Set.mem_iInter, Sum.forall, Finset.inl_mem_disjSum, Finset.mem_toLeft,        Finset.inr_mem_disjSum, Finset.mem_toRight, Set.mem_inter_iff, Set.mem_preimage,        Set.mem_setOf_eq, Subtype.forall, S, T]      congr! with i hi i hi <;> simp [← (hF _ hi).2]    · ext ω      simp only [Finset.mem_toLeft, Set.mem_iInter, Set.mem_preimage, Set.mem_setOf_eq,        Subtype.forall, S]      congr! with i hi      simp [← (hF _ hi).2]    · ext ω      simp only [Finset.mem_toRight, Set.mem_iInter, Set.mem_preimage, Set.mem_setOf_eq,        Subtype.forall, T]      congr! with i hi      simp [← (hF _ hi).2]    all_goals {      apply MeasurableSet.iInter; intro ⟨i, hi⟩      simp only      convert! measurableSet_preimage (measurable_pi_apply i) _      apply (hF _ _).1    }  · intro i hi; apply hE; exact Finset.mem_toRight.mp hi  intro j hj; apply hE; exact Finset.mem_toLeft.mp hj