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

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᶠ[ae μ] 0
h' : X * Y =ᶠ[ae μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
simp only [integral_congr_ae h'X, integral_congr_ae h', Pi.zero_apply, integral_const,
  Algebra.id.smul_eq_mul, mul_zero, zero_mul]

Result:
no goals

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
h'Y : ¬Y =ᶠ[ae μ] 0
h : Integrable (X * Y) μ
HX : Integrable X μ
HY : Integrable Y μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
exact hXY.integral_mul_of_integrable HX HY

Result:
no goals

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᶠ[ae μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have h' : X * Y =ᵐ[μ] 0 := by
  filter_upwards [h'X] with ω hω
  simp [hω]

Result:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᶠ[ae μ] 0
h' : X * Y =ᶠ[ae μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
h'Y : ¬Y =ᶠ[ae μ] 0
h : ¬Integrable (X * Y) μ
I : ¬(Integrable X μ ∧ Integrable Y μ)
⊢ 0 = integral μ X * integral μ Y

Tactic:
rw [not_and_or] at I

Result:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
h'Y : ¬Y =ᶠ[ae μ] 0
h : ¬Integrable (X * Y) μ
I : ¬Integrable X μ ∨ ¬Integrable Y μ
⊢ 0 = integral μ X * integral μ Y

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
h'Y : ¬Y =ᶠ[ae μ] 0
h : Integrable (X * Y) μ
HX : Integrable X μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have HY : Integrable Y μ := hXY.integrable_right_of_integrable_mul h hX hY h'X

Result:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
h'Y : ¬Y =ᶠ[ae μ] 0
h : Integrable (X * Y) μ
HX : Integrable X μ
HY : Integrable Y μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
h'Y : ¬Y =ᶠ[ae μ] 0
h : ¬Integrable (X * Y) μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
rw [integral_undef h]

Result:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
h'Y : ¬Y =ᶠ[ae μ] 0
h : ¬Integrable (X * Y) μ
⊢ 0 = integral μ X * integral μ Y