-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_Indep : iIndepFun (β := β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
have have₁ have₂ :
  ∀
    (h_right :
      f k =
        (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
            p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
          fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a),
    IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ
have₃ have₄ :
  ∀
    (h_right :
      f k =
        (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
            p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
          fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
        fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)),
    IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ
have₅ :
  ∀
    (h_right :
      f k =
        (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
            p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
          fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
        fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)),
    let s : Finset ι := {i, j};
    ∀
      (h_left :
        Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
          ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
              (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
            fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)),
      IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ
have₆ :
  ∀
    (h_right :
      f k =
        (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
            p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
          fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
        fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)),
    let s : Finset ι := {i, j};
    ∀
      (h_left :
        Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
          ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
              (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
            fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a))
      (h_meas_left :
        Measurable (β :=
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι) × β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯) : ι))
          fun (p : (l : ↥s) → β (↑l : ι)) ↦
          (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))),
      IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ
have₇ :
  ∀
    (h_right :
      f k =
        (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
            p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
          fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
        fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)),
    let s : Finset ι := {i, j};
    ∀
      (h_left :
        Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
          ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
              (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
            fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a))
      (h_meas_left :
        Measurable (β :=
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι) × β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯) : ι))
          fun (p : (l : ↥s) → β (↑l : ι)) ↦
          (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))),
      IndepFun.{u_1, u_2, u_8, u_8} (β := β i × β j) (γ := β k)
        ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
            (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
          fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
        ((fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
            p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
          fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
        κ μ
have₈ :
  ∀
    (h_right :
      f k =
        (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
            p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
          fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
        fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)),
    let s : Finset ι := {i, j};
    ∀
      (h_left :
        Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
          ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
              (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
            fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a))
      (h_meas_left :
        Measurable (β :=
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι) × β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯) : ι))
          fun (p : (l : ↥s) → β (↑l : ι)) ↦
          (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))),
      Disjoint s {k}
have₉ :
  ∀
    (h_right :
      f k =
        (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
            p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
          fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
        fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)),
    let s : Finset ι := {i, j};
    ∀
      (h_left :
        Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
          ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
              (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
            fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a))
      (h_meas_left :
        Measurable (β :=
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι) × β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯) : ι))
          fun (p : (l : ↥s) → β (↑l : ι)) ↦
          (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))),
      k ∉ s
have₁₀ :
  ∀
    (h_right :
      f k =
        (fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
            p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)) ∘
          fun (a : Ω) (j : ↥{k}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯) : ι))
        fun (p : (j : ↥{k}) → β (↑j : ι)) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {k} x) k ⋯)),
    let s : Finset ι := {i, j};
    ∀
      (h_left :
        Eq (α := (ω : Ω) → β i × β j) (fun (ω : Ω) ↦ (f i ω, f j ω))
          ((fun (p : (l : ↥s) → β (↑l : ι)) ↦
              (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))) ∘
            fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a))
      (h_meas_left :
        Measurable (β :=
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι) × β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯) : ι))
          fun (p : (l : ↥s) → β (↑l : ι)) ↦
          (p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯), p (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j ⋯))),
      ¬k = i ∧ ¬k = j
⊢ IndepFun (β := β i × β j) (fun (a : Ω) ↦ (f i a, f j a)) (f k) κ μ

Tactic:
classical
  have h_right :
      f k = (fun p : ∀ j : ({k} : Finset ι), β j => p ⟨k, Finset.mem_singleton_self k⟩) ∘
        fun a (j : ({k} : Finset ι)) => f j a :=
    rfl
  have h_meas_right : Measurable fun p : ∀ j : ({k} : Finset ι),
      β j => p ⟨k, Finset.mem_singleton_self k⟩ :=
    measurable_pi_apply _
  let s : Finset ι := {i, j}
  have h_left : (fun ω => (f i ω, f j ω)) = (fun p : ∀ l : s, β l =>
      (p ⟨i, Finset.mem_insert_self i _⟩,
        p ⟨j, Finset.mem_insert_of_mem (Finset.mem_singleton_self _)⟩)) ∘
        fun a (j : s) => f j a := by
    ext1 a
    simp only
    constructor
  have h_meas_left : Measurable fun p : ∀ l : s, β l =>
      (p ⟨i, Finset.mem_insert_self i _⟩,
        p ⟨j, Finset.mem_insert_of_mem (Finset.mem_singleton_self _)⟩) :=
    Measurable.prod (measurable_pi_apply _) (measurable_pi_apply _)
  rw [h_left, h_right]
  refine (hf_Indep.indepFun_finset s {k} ?_ hf_meas).comp h_meas_left h_meas_right
  rw [Finset.disjoint_singleton_right]
  simp only [s, Finset.mem_insert, Finset.mem_singleton, not_or]
  exact ⟨hik.symm, hjk.symm⟩

Premises used: Finset.mem_singleton, Finset.mem_insert, not_or, Finset.disjoint_singleton_right