-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem condExp_stronglyMeasurable_mul_of_bound₀ (hm : m ≤ m0) [IsFiniteMeasure μ] {f g : α → ℝ}
    (hf : AEStronglyMeasurable[m] f μ) (hg : Integrable g μ) (c : ℝ)
    (hf_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) : μ[f * g|m] =ᵐ[μ] f * μ[g|m]

Proof state:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * μ[g|m]
x : α
hxc : ‖f x‖ ≤ c
hx_eq : f x = AEStronglyMeasurable.mk f hf x
⊢ ‖AEStronglyMeasurable.mk f hf x‖ ≤ c

Tactic:
rwa [← hx_eq]

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
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 μ] AEStronglyMeasurable.mk f hf * μ[g|m]

Tactic:
refine condExp_stronglyMeasurable_mul_of_bound hm hf.stronglyMeasurable_mk hg c ?_

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * μ[g|m]
⊢ ∀ᵐ (x : α) ∂μ, ‖AEStronglyMeasurable.mk f hf x‖ ≤ c

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
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 EventuallyEq.trans ?_ this.symm

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
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 μ] AEStronglyMeasurable.mk f hf * μ[g|m]

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
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] := EventuallyEq.mul hf.ae_eq_mk EventuallyEq.rfl

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
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 α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

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

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
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 α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
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 α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
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 α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * μ[g|m]
⊢ ∀ᵐ (x : α) ∂μ, ‖AEStronglyMeasurable.mk f hf x‖ ≤ c

Tactic:
filter_upwards [hf_bound, hf.ae_eq_mk] with x hxc hx_eq

Result:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this✝ : μ[f * g|m] =ᶠ[ae μ] μ[AEStronglyMeasurable.mk f hf * g|m]
this : f * μ[g|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf * μ[g|m]
x : α
hxc : ‖f x‖ ≤ c
hx_eq : f x = AEStronglyMeasurable.mk f hf x
⊢ ‖AEStronglyMeasurable.mk f hf x‖ ≤ c