-- 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:
α : 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, ⋯⟩
⊢ ∏ j ∈ s, f j = (fun p => ∏ j : { x // x ∈ s }, p j) ∘ fun a j => f (↑j) a

Tactic:
ext1 a

Result:
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 : Ω
⊢ (∏ j ∈ s, f j) a = ((fun p => ∏ j : { x // x ∈ s }, p j) ∘ fun a j => f (↑j) a) 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
h_right : f i = (fun p => p ⟨i, ⋯⟩) ∘ fun a j => f (↑j) a
h_meas_right : Measurable fun p => p ⟨i, ⋯⟩
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ

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

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
⊢ 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
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ

Tactic:
have h_meas_right : Measurable fun p : ({i} : Finset ι) → β =>
    p ⟨i, Finset.mem_singleton_self i⟩ := measurable_pi_apply _

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, ⋯⟩
⊢ 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 : Ω
⊢ (∏ j ∈ s, f j) a = ∏ x : { x // x ∈ s }, f (↑x) a

Tactic:
have : (∏ j : ↥s, f (↑j) a) = (∏ j : ↥s, f ↑j) a := by rw [Finset.prod_apply]

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

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 : Ω
⊢ (∏ j ∈ s, f j) a = ((fun p => ∏ j : { x // x ∈ s }, p j) ∘ fun a j => f (↑j) a) a

Tactic:
simp only [Function.comp_apply]

Result:
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 : Ω
⊢ (∏ j ∈ s, f j) a = ∏ x : { x // x ∈ s }, f (↑x) 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
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) κ μ

Tactic:
exact
  (hf_Indep.indepFun_finset s {i} (Finset.disjoint_singleton_left.mpr hi).symm hf_meas).comp
    h_meas_left h_meas_right

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
⊢ 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_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

Result:
no goals