ProbabilityTheory.iIndepFun.finsets_comp'

lemma iIndepFun.finsets_comp' {f : ∀ i, Ω → β i} {S S' : Finset ι} (h_disjoint : Disjoint S S')    (hf_Indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i))    {γ γ' : Type u} {mγ : MeasurableSpace γ} {mγ' : MeasurableSpace γ'}    {φ : (∀ i : S, β i) → γ} {φ' : (∀ i : S', β i) → γ'} (hφ : Measurable φ) (hφ' : Measurable φ') :    IndepFun (fun a ↦ φ (fun (i : S) ↦ f i a)) (fun a ↦ φ' (fun (i : S') ↦ f i a)) μ := by  set S₂ := ![S,S']  set γ₂ := ![γ,γ']  set φ₂ : (j:Fin 2) → ((i: S₂ j) → β i) → γ₂ j :=    fun j =>      match j with      | 0 => φ      | 1 => φ'  have h_disjoint₂ : Set.PairwiseDisjoint Set.univ S₂ := by    simp_rw [Set.PairwiseDisjoint, Set.Pairwise, Fin.forall_fin_two, Function.onFun]    simp [h_disjoint, h_disjoint.symm, S₂]  set mγ₂ : (j:Fin 2) → MeasurableSpace (γ₂ j) := fun j ↦ match j with  | 0 => mγ  | 1 => mγ'  have hφ₂ (j:Fin 2) : Measurable (φ₂ j) := match j with  | 0 => hφ  | 1 => hφ'  have hneq : (0:Fin 2) ≠ (1:Fin 2) := by simp  simpa [φ₂, γ₂] using!    (iIndepFun.finsets_comp S₂ h_disjoint₂ hf_Indep hf_meas φ₂ hφ₂).indepFun hneq