-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem condExp_stronglyMeasurable_simpleFunc_mul (hm : m ≤ m0) (f : @SimpleFunc α m ℝ) {g : α → ℝ}
    (hg : Integrable g μ) : μ[(f * g : α → ℝ)|m] =ᵐ[μ] f * μ[g|m]

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)
g₁ g₂ : SimpleFunc α ℝ
x✝ : Disjoint (Function.support ⇑g₁) (Function.support ⇑g₂)
h_eq₁ : (fun f => μ[⇑f * g|m] =ᶠ[ae μ] ⇑f * μ[g|m]) g₁
h_eq₂ : (fun f => μ[⇑f * g|m] =ᶠ[ae μ] ⇑f * μ[g|m]) g₂
h_add : ⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
⊢ μ[⇑g₁ * g + ⇑g₂ * g|m] =ᶠ[ae μ] μ[⇑g₁ * g|m] + μ[⇑g₂ * g|m]

Tactic:
exact condExp_add (hg.simpleFunc_mul' hm _) (hg.simpleFunc_mul' hm _) _

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
⊢ s.indicator (μ[c • g|m]) =ᶠ[ae μ] s.indicator (c • μ[g|m])

Tactic:
filter_upwards [condExp_smul c g m] with x hx

Result:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
x : α
hx : (μ[c • g|m]) x = (c • μ[g|m]) x
⊢ s.indicator (μ[c • g|m]) x = s.indicator (c • μ[g|m]) x

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
⊢ μ[s.indicator (Function.const α c) * g|m] =ᶠ[ae μ] s.indicator (Function.const α c) * μ[g|m]

Tactic:
rw [this, this]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
⊢ μ[s.indicator (c • g)|m] =ᶠ[ae μ] s.indicator (c • μ[g|m])

Proof state:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
s : Set α
c : ℝ
f : α → ℝ
x : α
hx : x ∈ s
⊢ (s.indicator (Function.const α c) * f) x = s.indicator (c • f) x

Tactic:
simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul,
  Function.const_apply]

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)
g₁ g₂ : SimpleFunc α ℝ
x✝ : Disjoint (Function.support ⇑g₁) (Function.support ⇑g₂)
h_eq₁ : (fun f => μ[⇑f * g|m] =ᶠ[ae μ] ⇑f * μ[g|m]) g₁
h_eq₂ : (fun f => μ[⇑f * g|m] =ᶠ[ae μ] ⇑f * μ[g|m]) g₂
h_add : ⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
⊢ ⇑g₁ * μ[g|m] + ⇑g₂ * μ[g|m] =ᶠ[ae μ] ⇑(g₁ + g₂) * μ[g|m]

Tactic:
rw [h_add, add_mul]

Result:
no goals

Proof state:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
x : α
hx : (μ[c • g|m]) x = (c • μ[g|m]) x
⊢ s.indicator (μ[c • g|m]) x = s.indicator (c • μ[g|m]) x

Tactic:
classical simp_rw [Set.indicator_apply, hx]

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)
g₁ g₂ : SimpleFunc α ℝ
x✝ : Disjoint (Function.support ⇑g₁) (Function.support ⇑g₂)
h_eq₁ : (fun f => μ[⇑f * g|m] =ᶠ[ae μ] ⇑f * μ[g|m]) g₁
h_eq₂ : (fun f => μ[⇑f * g|m] =ᶠ[ae μ] ⇑f * μ[g|m]) g₂
h_add : ⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
⊢ μ[⇑(g₁ + g₂) * g|m] =ᶠ[ae μ] ⇑(g₁ + g₂) * μ[g|m]

Tactic:
calc
  μ[⇑(g₁ + g₂) * g|m] =ᵐ[μ] μ[(⇑g₁ + ⇑g₂) * g|m] := by
    refine condExp_congr_ae (EventuallyEq.mul ?_ EventuallyEq.rfl); rw [h_add]
  _ =ᵐ[μ] μ[⇑g₁ * g|m] + μ[⇑g₂ * g|m] := by
    rw [add_mul]; exact condExp_add (hg.simpleFunc_mul' hm _) (hg.simpleFunc_mul' hm _) _
  _ =ᵐ[μ] ⇑g₁ * μ[g|m] + ⇑g₂ * μ[g|m] := EventuallyEq.add h_eq₁ h_eq₂
  _ =ᵐ[μ] ⇑(g₁ + g₂) * μ[g|m] := by rw [h_add, add_mul]

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
⊢ μ[⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) * g|m] =ᶠ[ae μ]
    ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) * μ[g|m]

Tactic:
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise,
  SimpleFunc.coe_const, SimpleFunc.coe_zero, Set.piecewise_eq_indicator]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
⊢ μ[s.indicator (Function.const α c) * g|m] =ᶠ[ae μ] s.indicator (Function.const α c) * μ[g|m]

Proof state:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
s : Set α
c : ℝ
f : α → ℝ
x : α
⊢ (s.indicator (Function.const α c) * f) x = s.indicator (c • f) x

Tactic:
by_cases hx : x ∈ s

Result:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
s : Set α
c : ℝ
f : α → ℝ
x : α
hx : x ∈ s
⊢ (s.indicator (Function.const α c) * f) x = s.indicator (c • f) x

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g μ
s : Set α
c : ℝ
f : α → ℝ
x : α
hx : x ∉ s
⊢ (s.indicator (Function.const α c) * f) x = s.indicator (c • f) x