-- Mathlib/Probability/Integration.lean
theorem IndepFun.integrable_right_of_integrable_mul {β : Type*} [MeasurableSpace β] {X Y : Ω → β}
    [NormedDivisionRing β] [BorelSpace β] (hXY : IndepFun X Y μ) (h'XY : Integrable (X * Y) μ)
    (hX : AEStronglyMeasurable X μ) (hY : AEStronglyMeasurable Y μ) (h'X : ¬X =ᵐ[μ] 0) :
    Integrable Y μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
H : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ = 0
I : (fun x => ‖X x‖ₑ) =ᶠ[ae μ] 0
⊢ False

Tactic:
apply h'X

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
H : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ = 0
I : (fun x => ‖X x‖ₑ) =ᶠ[ae μ] 0
⊢ X =ᶠ[ae μ] 0

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ = ⊤
J : IndepFun (fun ω => ‖X ω‖ₑ) (fun ω => ‖Y ω‖ₑ) μ
⊢ False

Tactic:
have A : ∫⁻ ω, ‖X ω * Y ω‖ₑ ∂μ < ∞ := h'XY.2

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ = ⊤
J : IndepFun (fun ω => ‖X ω‖ₑ) (fun ω => ‖Y ω‖ₑ) μ
A : ∫⁻ (ω : Ω), ‖X ω * Y ω‖ₑ ∂μ < ⊤
⊢ False

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ = ⊤
⊢ False

Tactic:
have J : IndepFun (fun ω => ‖X ω‖ₑ : Ω → ℝ≥0∞) (fun ω => ‖Y ω‖ₑ : Ω → ℝ≥0∞) μ :=
  IndepFun.comp hXY measurable_enorm measurable_enorm

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ = ⊤
J : IndepFun (fun ω => ‖X ω‖ₑ) (fun ω => ‖Y ω‖ₑ) μ
⊢ False

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
H : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ = 0
I : (fun x => ‖X x‖ₑ) =ᶠ[ae μ] 0
⊢ X =ᶠ[ae μ] 0

Tactic:
filter_upwards [I] with ω hω

Result:
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
H : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ = 0
I : (fun x => ‖X x‖ₑ) =ᶠ[ae μ] 0
ω : Ω
hω : ‖X ω‖ₑ = 0 ω
⊢ X ω = 0 ω

Proof state:
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
H : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ = 0
I : (fun x => ‖X x‖ₑ) =ᶠ[ae μ] 0
ω : Ω
hω : ‖X ω‖ₑ = 0 ω
⊢ X ω = 0 ω

Tactic:
simpa using hω

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
⊢ Integrable Y μ

Tactic:
refine ⟨hY, ?_⟩

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
⊢ HasFiniteIntegral Y μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ = ⊤
J : IndepFun (fun ω => ‖X ω‖ₑ) (fun ω => ‖Y ω‖ₑ) μ
A : (∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ⊤ < ⊤
⊢ False

Tactic:
simp only [ENNReal.mul_top I, lt_self_iff_false] at A

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ = ⊤
J : IndepFun (fun ω => ‖X ω‖ₑ) (fun ω => ‖Y ω‖ₑ) μ
A : ∫⁻ (ω : Ω), ‖X ω * Y ω‖ₑ ∂μ < ⊤
⊢ False

Tactic:
simp only [enorm_mul, ENNReal.coe_mul] at A

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ = ⊤
J : IndepFun (fun ω => ‖X ω‖ₑ) (fun ω => ‖Y ω‖ₑ) μ
A : ∫⁻ (ω : Ω), ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ < ⊤
⊢ False

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ = ⊤
J : IndepFun (fun ω => ‖X ω‖ₑ) (fun ω => ‖Y ω‖ₑ) μ
A : ∫⁻ (ω : Ω), ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ < ⊤
⊢ False

Tactic:
rw [lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.enorm hY.enorm J, H] at A

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ = ⊤
J : IndepFun (fun ω => ‖X ω‖ₑ) (fun ω => ‖Y ω‖ₑ) μ
A : (∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ⊤ < ⊤
⊢ False