-- Mathlib/Probability/Density.lean
theorem hasFiniteIntegral_mul {f : ℝ → ℝ} {g : ℝ → ℝ≥0∞} (hg : pdf X ℙ =ᵐ[volume] g)
    (hgi : ∫⁻ x, ‖f x‖ₑ * g x ≠ ∞) :
    HasFiniteIntegral fun x => f x * (pdf X ℙ volume x).toReal

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
⊢ (fun x => ENNReal.ofReal (pdf X ℙ volume x).toReal) =ᶠ[ae volume] fun x => ‖(pdf X ℙ volume x).toReal‖ₑ

Tactic:
simp only [Real.enorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
⊢ (fun x => ‖f x‖ₑ * g x) =ᶠ[ae volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖ₑ

Tactic:
refine ae_eq_trans ((ae_eq_refl _).mul (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) ?_

Result:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
⊢ (fun x => ‖f x‖ₑ * ENNReal.ofReal (pdf X ℙ volume x).toReal) =ᶠ[ae volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖ₑ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
⊢ (fun x => ‖f x‖ₑ * ENNReal.ofReal (pdf X ℙ volume x).toReal) =ᶠ[ae volume] fun x =>
    ‖f x‖ₑ * ‖(pdf X ℙ volume x).toReal‖ₑ

Tactic:
refine .mul (ae_eq_refl _) ?_

Result:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
⊢ (fun x => ENNReal.ofReal (pdf X ℙ volume x).toReal) =ᶠ[ae volume] fun x => ‖(pdf X ℙ volume x).toReal‖ₑ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
⊢ (fun x => ‖f x‖ₑ * ENNReal.ofReal (pdf X ℙ volume x).toReal) =ᶠ[ae volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖ₑ

Tactic:
simp_rw [← smul_eq_mul, enorm_smul, smul_eq_mul]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
⊢ (fun x => ‖f x‖ₑ * ENNReal.ofReal (pdf X ℙ volume x).toReal) =ᶠ[ae volume] fun x =>
    ‖f x‖ₑ * ‖(pdf X ℙ volume x).toReal‖ₑ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
this : (fun x => ‖f x‖ₑ * g x) =ᶠ[ae volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖ₑ
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ⊤

Tactic:
rwa [lt_top_iff_ne_top, ← lintegral_congr_ae this]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
⊢ HasFiniteIntegral (fun x => f x * (pdf X ℙ volume x).toReal) volume

Tactic:
rw [hasFiniteIntegral_iff_enorm]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ⊤

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ⊤

Tactic:
have : (fun x => ‖f x‖ₑ * g x) =ᵐ[volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖ₑ := by
  refine ae_eq_trans ((ae_eq_refl _).mul (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) ?_
  simp_rw [← smul_eq_mul, enorm_smul, smul_eq_mul]
  refine .mul (ae_eq_refl _) ?_
  simp only [Real.enorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤
this : (fun x => ‖f x‖ₑ * g x) =ᶠ[ae volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖ₑ
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ⊤