-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepFun.indepFun_finset_prod_of_not_mem (hf_Indep : iIndepFun (fun _ ↦ m) f κ μ)
    (hf_meas : ∀ i, Measurable (f i)) {s : Finset ι} {i : ι} (hi : i ∉ s) :
    IndepFun (∏ j ∈ s, f j) (f i) κ μ

Proof state:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p => p ⟨i, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨i, ⋯⟩
a : Ω
this : ∏ j : { x // x ∈ s }, f (↑j) a = (∏ j : { x // x ∈ s }, f ↑j) a
⊢ (∏ j ∈ s, f j) a = ∏ x : { x // x ∈ s }, f (↑x) a

Tactic:
rw [this, Finset.prod_coe_sort]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p => p ⟨i, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨i, ⋯⟩
a : Ω
⊢ ∏ j : { x // x ∈ s }, f (↑j) a = (∏ j : { x // x ∈ s }, f ↑j) a

Tactic:
rw [Finset.prod_apply]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p => p ⟨i, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨i, ⋯⟩
h_left : ∏ j ∈ s, f j = (fun p => ∏ j : { x // x ∈ s }, p j) ∘ fun a j => f (↑j) a
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ

Tactic:
have h_meas_left : Measurable fun p : s → β => ∏ j, p j :=
  Finset.univ.measurable_prod fun (j : ↥s) (_H : j ∈ Finset.univ) => measurable_pi_apply j

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p => p ⟨i, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨i, ⋯⟩
h_left : ∏ j ∈ s, f j = (fun p => ∏ j : { x // x ∈ s }, p j) ∘ fun a j => f (↑j) a
h_meas_left : Measurable fun p => ∏ j : { x // x ∈ s }, p j
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p => p ⟨i, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨i, ⋯⟩
h_left : ∏ j ∈ s, f j = (fun p => ∏ j : { x // x ∈ s }, p j) ∘ fun a j => f (↑j) a
h_meas_left : Measurable fun p => ∏ j : { x // x ∈ s }, p j
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ

Tactic:
rw [h_left, h_right]

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p => p ⟨i, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨i, ⋯⟩
h_left : ∏ j ∈ s, f j = (fun p => ∏ j : { x // x ∈ s }, p j) ∘ fun a j => f (↑j) a
h_meas_left : Measurable fun p => ∏ j : { x // x ∈ s }, p j
⊢ IndepFun ((fun p => ∏ j : { x // x ∈ s }, p j) ∘ fun a j => f (↑j) a) ((fun p => p ⟨i, ⋯⟩) ∘ fun a j => f (↑j) a) κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ

Tactic:
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

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p => p ⟨i, ⋯⟩) ∘ fun a j => f (↑j) a
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ