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

Proof state:
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g) μ
hg : Integrable g μ
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
sets : ℕ → Set α
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ⊤
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
⊢ μ.restrict (sets n)[(sets n).indicator f * g|m] =ᶠ[ae (μ.restrict (sets n))]
    (sets n).indicator f * μ.restrict (sets n)[g|m]

Tactic:
have : IsFiniteMeasure (μ.restrict (sets n)) := by
  constructor
  rw [Measure.restrict_apply_univ]
  exact h_finite n

Result:
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g) μ
hg : Integrable g μ
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
sets : ℕ → Set α
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ⊤
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
this : IsFiniteMeasure (μ.restrict (sets n))
⊢ μ.restrict (sets n)[(sets n).indicator f * g|m] =ᶠ[ae (μ.restrict (sets n))]
    (sets n).indicator f * μ.restrict (sets n)[g|m]

Proof state:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g) μ
hg : Integrable g μ
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
sets : ℕ → Set α
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ⊤
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
this :
  μ.restrict (sets n)[(sets n).indicator f * g|m] =ᶠ[ae (μ.restrict (sets n))]
    (sets n).indicator f * μ.restrict (sets n)[g|m]
⊢ (sets n).indicator f * μ.restrict (sets n)[g|m] =ᶠ[ae (μ.restrict (sets n))] f * μ.restrict (sets n)[g|m]

Tactic:
exact (indicator_ae_eq_restrict <| hm _ <| h_meas n).mul EventuallyEq.rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g) μ
hg : Integrable g μ
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
haveI : SigmaFinite (μ.trim hm) := hμm

Result:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g) μ
hg : Integrable g μ
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Proof state:
case pos.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g) μ
hg : Integrable g μ
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
sets : ℕ → Set α
h_univ : ⋃ i, sets i = Set.univ
sets_prop : (∀ (x : ℕ), MeasurableSet (sets x)) ∧ (∀ (x : ℕ), μ (sets x) < ⊤) ∧ ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
obtain ⟨h_meas, h_finite, h_norm⟩ := sets_prop

Result:
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g) μ
hg : Integrable g μ
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
sets : ℕ → Set α
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ⊤
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

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

Tactic:
simp_rw [condExp_of_not_le hm]

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g) μ
hg : Integrable g μ
hm : ¬m ≤ m0
⊢ 0 =ᶠ[ae μ] f * 0

Proof state:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g) μ
hg : Integrable g μ
hm : ¬m ≤ m0
⊢ 0 =ᶠ[ae μ] f * 0

Tactic:
rw [mul_zero]

Result:
no goals