-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem condExp_mul_of_aestronglyMeasurable_left {f g : α → ℝ} (hf : AEStronglyMeasurable[m] f μ)
    (hfg : Integrable (f * g) μ) (hg : Integrable g μ) : μ[f * g|m] =ᵐ[μ] f * μ[g|m]

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
this : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
refine this.trans ?_

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
this : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
⊢ μ[AEStronglyMeasurable.mk f hf * g|m] =ᶠ[ae μ] f * μ[g|m]

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
this : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
⊢ μ[AEStronglyMeasurable.mk f hf * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
have : f * μ[g|m] =ᵐ[μ] hf.mk f * μ[g|m] := hf.ae_eq_mk.mul EventuallyEq.rfl

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * μ[g|m]
⊢ μ[AEStronglyMeasurable.mk f hf * g|m] =ᶠ[ae μ] f * μ[g|m]

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * μ[g|m]
⊢ f * g =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * g

Tactic:
exact hf.ae_eq_mk.mul EventuallyEq.rfl

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * μ[g|m]
⊢ Integrable (AEStronglyMeasurable.mk f hf * g) μ

Tactic:
refine (integrable_congr ?_).mp hfg

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * μ[g|m]
⊢ f * g =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * g

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
have : μ[f * g|m] =ᵐ[μ] μ[hf.mk f * g|m] :=
  condExp_congr_ae (hf.ae_eq_mk.mul EventuallyEq.rfl)

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
this : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * μ[g|m]
⊢ μ[AEStronglyMeasurable.mk f hf * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
refine (condExp_mul_of_stronglyMeasurable_left hf.stronglyMeasurable_mk ?_ hg).trans this.symm

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * μ[g|m]
⊢ Integrable (AEStronglyMeasurable.mk f hf * g) μ