-- 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 intro
Ω : 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 μ
⊢ False

Tactic:
exact h (hXY.integrable_mul HX HY)

Result:
no goals

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

Tactic:
filter_upwards [h'X] with ω hω

Result:
case h
Ω : 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 ω = 0 ω
⊢ (X * Y) ω = 0 ω

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hXY : IndepFun X Y μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
by_cases h'X : X =ᵐ[μ] 0

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
⊢ integral μ (X * Y) = integral μ X * integral μ Y

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
⊢ 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'Y : ¬Y =ᶠ[ae μ] 0
h : Integrable (X * Y) μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have HX : Integrable X μ := hXY.integrable_left_of_integrable_mul h hX hY h'Y

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 μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
Ω : 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
⊢ X * Y =ᶠ[ae μ] 0

Tactic:
filter_upwards [h'Y] with ω hω

Result:
case h
Ω : 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ω : Y ω = 0 ω
⊢ (X * Y) ω = 0 ω

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:
rcases I with I | I <;> simp [integral_undef I]

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
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
have h' : X * Y =ᵐ[μ] 0 := by
  filter_upwards [h'Y] 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'Y : Y =ᶠ[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) μ
⊢ 0 = integral μ X * integral μ Y

Tactic:
have I : ¬(Integrable X μ ∧ Integrable Y μ) := by
  rintro ⟨HX, HY⟩
  exact h (hXY.integrable_mul HX HY)

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' : X * Y =ᶠ[ae μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y

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

Result:
no goals

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
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
by_cases h'Y : Y =ᵐ[μ] 0

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
⊢ integral μ (X * Y) = integral μ X * integral μ Y

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
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Proof state:
Ω : 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) μ
⊢ ¬(Integrable X μ ∧ Integrable Y μ)

Tactic:
rintro ⟨HX, HY⟩

Result:
case intro
Ω : 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 μ
⊢ False

Proof state:
case h
Ω : 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ω : Y ω = 0 ω
⊢ (X * Y) ω = 0 ω

Tactic:
simp [hω]

Result:
no goals

Proof state:
case h
Ω : 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 ω = 0 ω
⊢ (X * Y) ω = 0 ω

Tactic:
simp [hω]

Result:
no goals

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
⊢ integral μ (X * Y) = integral μ X * integral μ Y

Tactic:
by_cases h : Integrable (X * Y) μ

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) μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y

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