ProbabilityTheory.iIndepFun.pair_last_of_three

lemma pair_last_of_three    (hZ₁ : Measurable Z₁) (hZ₂ : Measurable Z₂) (hZ₃ : Measurable Z₃) :    IndepFun Z₁ (⟨Z₂, Z₃⟩) := by  have T := iIndepFun.pi' (m := fun _ _ ↦ hG) ?_ (h_indep.precomp κ_equiv.injective); swap  · rintro ⟨i, j⟩; fin_cases i <;> fin_cases j <;> assumption  -- apply to this pair of independent variables the function mapping the latter pair (as  -- a function on `Fin 2`) to the same pair, but in the product space sense.  -- It retains independence, proving the conclusion.  let phi_third : ∀ (i : Fin 2), (κ i → G) → (self_or_prod G i)    | 0 => (fun f ↦ f ⟨0, zero_lt_one⟩)    | 1 => (fun f ↦ (f ⟨0, zero_lt_two⟩, f ⟨1, one_lt_two⟩))  let M i : MeasurableSpace (self_or_prod G i) := by match i with | 0 | 1 => infer_instance  have := T.comp phi_third  refine (this ?_).indepFun (i := 0) (j := 1) zero_ne_one  intro i  match i with  | 0 | 1 => fun_prop