-- 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
α : 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 α
sets_prop : ∀ (n : ℕ), MeasurableSet (sets n) ∧ μ (sets n) < ⊤ ∧ ∀ x ∈ sets n, ‖f x‖ ≤ ↑n
h_univ : ⋃ i, sets i = Set.univ
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
simp_rw [forall_and] at sets_prop

Result:
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]

Proof state:
α : 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
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ sets n → (μ[f * g|m]) x = f x * (μ[g|m]) x
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
rw [← ae_all_iff] at this

Result:
α : 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
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
⊢ μ[f * g|m] =ᶠ[ae μ] 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
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
suffices ∀ n, ∀ᵐ x ∂μ, x ∈ sets n → (μ[f * g|m]) x = f x * (μ[g|m]) x by
  rw [← ae_all_iff] at this
  filter_upwards [this] with x hx
  obtain ⟨i, hi⟩ : ∃ i, x ∈ sets i := by
    have h_mem : x ∈ ⋃ i, sets i := by rw [h_univ]; exact Set.mem_univ _
    simpa using h_mem
  exact hx i hi

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 : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ sets n → (μ[f * g|m]) x = f x * (μ[g|m]) x

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
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᶠ[ae μ] f * 0

Tactic:
rw [mul_zero]

Result:
no goals

Proof state:
case h
α : 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
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
x : α
hx : ∀ (i : ℕ), x ∈ sets i → (μ[f * g|m]) x = f x * (μ[g|m]) x
⊢ (μ[f * g|m]) x = (f * μ[g|m]) x

Tactic:
obtain ⟨i, hi⟩ : ∃ i, x ∈ sets i := by
  have h_mem : x ∈ ⋃ i, sets i := by rw [h_univ]; exact Set.mem_univ _
  simpa using h_mem

Result:
case h.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
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
x : α
hx : ∀ (i : ℕ), x ∈ sets i → (μ[f * g|m]) x = f x * (μ[g|m]) x
i : ℕ
hi : x ∈ sets i
⊢ (μ[f * g|m]) x = (f * μ[g|m]) x

Proof state:
case refine_1
α : 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]
⊢ μ.restrict (sets n)[f * g|m] =ᶠ[ae (μ.restrict (sets n))] μ.restrict (sets n)[(sets n).indicator f * g|m]

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

Result:
no goals

Proof state:
case measure_univ_lt_top
α : 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 : ℕ
⊢ μ (sets n) < ⊤

Tactic:
exact h_finite n

Result:
no goals

Proof state:
α : 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
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
x : α
hx : ∀ (i : ℕ), x ∈ sets i → (μ[f * g|m]) x = f x * (μ[g|m]) x
⊢ x ∈ Set.univ

Tactic:
exact Set.mem_univ _

Result:
no goals

Proof state:
α : 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)[f * g|m] =ᶠ[ae (μ.restrict (sets n))] f * μ.restrict (sets n)[g|m]
⊢ μ.restrict (sets n)[f * g|m] =ᶠ[ae (μ.restrict (sets n))] fun x => f x * (μ[g|m]) x

Tactic:
exact this.trans (EventuallyEq.rfl.mul (condExp_restrict_ae_eq_restrict hm (h_meas n) hg))

Result:
no goals