-- 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 : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
have have₁ have₂ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a),
    IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have₃ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β) fun (p : ↥{i} → β) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)),
    IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have₄ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β) fun (p : ↥{i} → β) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
    (h_left :
      Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)),
    IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have₅ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β) fun (p : ↥{i} → β) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
    (h_left : Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a))
    (h_meas_left : Measurable (β := β) fun (p : ↥s → β) ↦ ∏ j : ↥s, p j), IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have₆ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β) fun (p : ↥{i} → β) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
    (h_left : Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a))
    (h_meas_left : Measurable (β := β) fun (p : ↥s → β) ↦ ∏ j : ↥s, p j),
    IndepFun.{u_1, u_2, u_8, u_8} (β := β) (γ := β)
      ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)
      ((fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
        fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
      κ μ
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ

Tactic:
classical
  have h_right : f i =
    (fun p : ({i} : Finset ι) → β => p ⟨i, Finset.mem_singleton_self i⟩) ∘
    fun a (j : ({i} : Finset ι)) => f j a := rfl
  have h_meas_right : Measurable fun p : ({i} : Finset ι) → β =>
      p ⟨i, Finset.mem_singleton_self i⟩ := measurable_pi_apply _
  have h_left : ∏ j ∈ s, f j = (fun p : s → β => ∏ j, p j) ∘ fun a (j : s) => f j a := by
    ext1 a
    simp only [Function.comp_apply]
    have : (∏ j : ↥s, f (↑j) a) = (∏ j : ↥s, f ↑j) a := by rw [Finset.prod_apply]
    rw [this, Finset.prod_coe_sort]
  have h_meas_left : Measurable fun p : s → β => ∏ j, p j :=
    Finset.univ.measurable_fun_prod fun (j : ↥s) (_H : j ∈ Finset.univ) => measurable_pi_apply j
  rw [h_left, h_right]
  exact
    (hf_Indep.indepFun_finset s {i} (Finset.disjoint_singleton_left.mpr hi).symm hf_meas).comp
      h_meas_left h_meas_right