-- Mathlib/Probability/Integration.lean
theorem IndepFun.integral_mul_of_integrable (hXY : IndepFun X Y μ) (hX : Integrable X μ)
    (hY : Integrable Y μ) : integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm μ
hm2 : AEMeasurable Xp μ
hm3 : AEMeasurable Ym μ
hm4 : AEMeasurable Yp μ
hv1 : Integrable Xm μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have hv2 : Integrable Xp μ := hX.pos_part

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm μ
hm2 : AEMeasurable Xp μ
hm3 : AEMeasurable Ym μ
hm4 : AEMeasurable Yp μ
hv1 : Integrable Xm μ
hv2 : Integrable Xp μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm μ
hm2 : AEMeasurable Xp μ
hm3 : AEMeasurable Ym μ
hm4 : AEMeasurable Yp μ
hv1 : Integrable Xm μ
hv2 : Integrable Xp μ
hv3 : Integrable Ym μ
hv4 : Integrable Yp μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have hi1 : IndepFun Xm Ym μ := hXY.comp negm negm

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm μ
hm2 : AEMeasurable Xp μ
hm3 : AEMeasurable Ym μ
hm4 : AEMeasurable Yp μ
hv1 : Integrable Xm μ
hv2 : Integrable Xp μ
hv3 : Integrable Ym μ
hv4 : Integrable Yp μ
hi1 : IndepFun Xm Ym μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have hp2 : 0 ≤ Xp := fun ω => le_max_right _ _

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have hp4 : 0 ≤ Yp := fun ω => le_max_right _ _

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm μ
hm2 : AEMeasurable Xp μ
hm3 : AEMeasurable Ym μ
hm4 : AEMeasurable Yp μ
hv1 : Integrable Xm μ
hv2 : Integrable Xp μ
hv3 : Integrable Ym μ
hv4 : Integrable Yp μ
hi1 : IndepFun Xm Ym μ
hi2 : IndepFun Xp Ym μ
hi3 : IndepFun Xm Yp μ
hi4 : IndepFun Xp Yp μ
hl1 : Integrable (Xm * Ym) μ
hl2 : Integrable (Xp * Ym) μ
hl3 : Integrable (Xm * Yp) μ
hl4 : Integrable (Xp * Yp) μ
hl5 : Integrable (Xp * Yp - Xm * Yp) μ
hl6 : Integrable (Xp * Ym - Xm * Ym) μ
⊢ integral μ (Xp * Yp - Xm * Yp - (Xp * Ym - Xm * Ym)) = integral μ (Xp - Xm) * integral μ (Yp - Ym)

Tactic:
rw [integral_sub' hl5 hl6, integral_sub' hl4 hl3, integral_sub' hl2 hl1, integral_sub' hv2 hv1,
  integral_sub' hv4 hv3, hi1.integral_mul_of_nonneg hp1 hp3 hm1 hm3,
  hi2.integral_mul_of_nonneg hp2 hp3 hm2 hm3, hi3.integral_mul_of_nonneg hp1 hp4 hm1 hm4,
  hi4.integral_mul_of_nonneg hp2 hp4 hm2 hm4]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm μ
hm2 : AEMeasurable Xp μ
hm3 : AEMeasurable Ym μ
hm4 : AEMeasurable Yp μ
hv1 : Integrable Xm μ
hv2 : Integrable Xp μ
hv3 : Integrable Ym μ
hv4 : Integrable Yp μ
hi1 : IndepFun Xm Ym μ
hi2 : IndepFun Xp Ym μ
hi3 : IndepFun Xm Yp μ
hi4 : IndepFun Xp Yp μ
hl1 : Integrable (Xm * Ym) μ
hl2 : Integrable (Xp * Ym) μ
hl3 : Integrable (Xm * Yp) μ
hl4 : Integrable (Xp * Yp) μ
hl5 : Integrable (Xp * Yp - Xm * Yp) μ
hl6 : Integrable (Xp * Ym - Xm * Ym) μ
⊢ integral μ Xp * integral μ Yp - integral μ Xm * integral μ Yp -
      (integral μ Xp * integral μ Ym - integral μ Xm * integral μ Ym) =
    (∫ (a : Ω), Xp a ∂μ - ∫ (a : Ω), Xm a ∂μ) * (∫ (a : Ω), Yp a ∂μ - ∫ (a : Ω), Ym a ∂μ)

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
let Ym := neg ∘ Y

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y