-- Mathlib/Probability/Integration.lean
theorem IndepFun.integral_mul_of_nonneg (hXY : IndepFun X Y μ) (hXp : 0 ≤ X) (hYp : 0 ≤ Y)
    (hXm : AEMeasurable X μ) (hYm : AEMeasurable Y μ) :
    integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ :=
  ENNReal.measurable_ofReal.comp_aemeasurable hYm

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
h4 : 0 ≤ᶠ[ae μ] X * Y
⊢ ∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ =
    (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ

Tactic:
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' h1 h2

Result:
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
h4 : 0 ≤ᶠ[ae μ] X * Y
⊢ IndepFun (fun a => ENNReal.ofReal (X a)) (fun a => ENNReal.ofReal (Y a)) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have h3 : AEMeasurable (X * Y) μ := hXm.mul hYm

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
h4 : 0 ≤ᶠ[ae μ] X * Y
⊢ (∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ).toReal =
    ((∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ).toReal

Tactic:
congr

Result:
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
h4 : 0 ≤ᶠ[ae μ] X * Y
⊢ ∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ =
    (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ

Proof state:
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
h4 : 0 ≤ᶠ[ae μ] X * Y
⊢ IndepFun (fun a => ENNReal.ofReal (X a)) (fun a => ENNReal.ofReal (Y a)) μ

Tactic:
exact hXY.comp ENNReal.measurable_ofReal ENNReal.measurable_ofReal

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
h4 : 0 ≤ᶠ[ae μ] X * Y
⊢ (∫⁻ (a : Ω), ENNReal.ofReal ((X * Y) a) ∂μ).toReal =
    (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ).toReal * (∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ).toReal

Tactic:
simp_rw [← ENNReal.toReal_mul, Pi.mul_apply, ENNReal.ofReal_mul (hXp _)]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
h4 : 0 ≤ᶠ[ae μ] X * Y
⊢ (∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ).toReal =
    ((∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ).toReal

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have h4 : 0 ≤ᵐ[μ] X * Y := ae_of_all _ fun ω => mul_nonneg (hXp ω) (hYp ω)

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
h4 : 0 ≤ᶠ[ae μ] X * Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
h4 : 0 ≤ᶠ[ae μ] X * Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ hXp) hXm.aestronglyMeasurable,
  integral_eq_lintegral_of_nonneg_ae (ae_of_all _ hYp) hYm.aestronglyMeasurable,
  integral_eq_lintegral_of_nonneg_ae h4 h3.aestronglyMeasurable]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ
h3 : AEMeasurable (X * Y) μ
h4 : 0 ≤ᶠ[ae μ] X * Y
⊢ (∫⁻ (a : Ω), ENNReal.ofReal ((X * Y) a) ∂μ).toReal =
    (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ).toReal * (∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ).toReal

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ :=
  ENNReal.measurable_ofReal.comp_aemeasurable hXm

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X μ
hYm : AEMeasurable Y μ
h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y