ProbabilityTheory.iIndepFun.apply_two_last

lemma apply_two_last    (hZ₁ : Measurable Z₁) (hZ₂ : Measurable Z₂) (hZ₃ : Measurable Z₃) (hZ₄ : Measurable Z₄)    {phi : G → G → G} (hphi : Measurable phi.uncurry) :    iIndepFun ![Z₁, Z₂, (fun ω ↦ phi (Z₃ ω) (Z₄ ω))] := by  -- deduce from the assumption the independence of `Z₁`, `Z₂` and `(Z₃, Z₄)`.  have T := (h_indep.precomp κ_equiv.injective).pi' (m := fun _ _ ↦ hG) ?_; swap  · rintro ⟨i, j⟩; fin_cases i <;> fin_cases j <;> assumption  -- apply to this triplet of independent variables the function `phi` applied to `Z₃` and `Z₄`  -- which does not change the other variables. It retains independence, proving the conclusion.  let phi_third : ∀ (i : Fin 3), (κ i → G) → G    | 0 | 1 => (fun f ↦ f ⟨0, zero_lt_one⟩)    | 2   => (fun f ↦ phi (f ⟨0, zero_lt_two⟩) (f ⟨1, one_lt_two⟩))  convert T.comp phi_third ?_ with i  · fin_cases i <;> rfl  · intro i    match i with    | 0 | 1 => exact measurable_pi_apply _    | 2 =>      have : Measurable (fun (p : Fin 2 → G) ↦ (p 0, p 1)) := by fun_prop      exact hphi.comp this