-- Mathlib/Probability/Integration.lean
theorem lintegral_prod_eq_prod_lintegral_of_indepFun {ι : Type*}
    (s : Finset ι) (X : ι → Ω → ℝ≥0∞)
    (hX : iIndepFun (fun _ ↦ ENNReal.measurableSpace) X μ)
    (x_mea : ∀ i, Measurable (X i)) :
    ∫⁻ ω, ∏ i ∈ s, (X i ω) ∂μ = ∏ i ∈ s, ∫⁻ ω, X i ω ∂μ

Proof state:
case cons
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ ∫⁻ (ω : Ω), (X j * ∏ c ∈ s, X c) ω ∂μ = (∫⁻ (ω : Ω), X j ω ∂μ) * ∫⁻ (ω : Ω), (∏ c ∈ s, X c) ω ∂μ

Tactic:
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'

Result:
case cons.h_meas_f
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ AEMeasurable (X j) μ

case cons.h_meas_g
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ AEMeasurable (∏ c ∈ s, X c) μ

case cons.h_indep_fun
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ IndepFun (X j) (∏ c ∈ s, X c) μ

Proof state:
case cons.h_indep_fun
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ IndepFun (X j) (∏ c ∈ s, X c) μ

Tactic:
exact (iIndepFun.indepFun_finset_prod_of_not_mem hX x_mea hj).symm

Result:
no goals

Proof state:
case cons
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ ∫⁻ (ω : Ω), ∏ i ∈ Finset.cons j s hj, X i ω ∂μ = ∏ i ∈ Finset.cons j s hj, ∫⁻ (ω : Ω), X i ω ∂μ

Tactic:
simp only [← Finset.prod_apply, Finset.prod_cons, ← ihs]

Result:
case cons
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ ∫⁻ (ω : Ω), (X j * ∏ c ∈ s, X c) ω ∂μ = (∫⁻ (ω : Ω), X j ω ∂μ) * ∫⁻ (ω : Ω), (∏ c ∈ s, X c) ω ∂μ

Proof state:
case empty
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
⊢ ∫⁻ (ω : Ω), ∏ i ∈ ∅, X i ω ∂μ = ∏ i ∈ ∅, ∫⁻ (ω : Ω), X i ω ∂μ

Tactic:
simp only [Finset.prod_empty, lintegral_const, measure_univ, mul_one]

Result:
no goals

Proof state:
case cons.h_meas_g
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ AEMeasurable (∏ c ∈ s, X c) μ

Tactic:
exact s.aemeasurable_prod' (fun i _ ↦ (x_mea i).aemeasurable)

Result:
no goals

Proof state:
case cons.h_meas_f
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ AEMeasurable (X j) μ

Tactic:
exact (x_mea j).aemeasurable

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
⊢ ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ

Tactic:
have : IsProbabilityMeasure μ := hX.isProbabilityMeasure

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (fun x => ENNReal.measurableSpace) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
⊢ ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ