-- 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₂
⊢ μ[⇑(g₁ + g₂) * g|m] =ᶠ[ae μ] ⇑(g₁ + g₂) * μ[g|m]

Tactic:
have h_add := @SimpleFunc.coe_add _ _ m _ g₁ g₂

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)
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]

Proof state:
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

Tactic:
simp only [hx, Pi.mul_apply, Set.indicator_of_not_mem, not_false_iff, zero_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)
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₂) =ᶠ[ae μ] ⇑g₁ + ⇑g₂

Tactic:
rw [h_add]

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)
⊢ μ[⇑f * g|m] =ᶠ[ae μ] ⇑f * μ[g|m]

Tactic:
apply @SimpleFunc.induction _ _ m _ (fun f => _)
  (fun c s hs => ?_) (fun g₁ g₂ _ h_eq₁ h_eq₂ => ?_) f

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
⊢ μ[⇑(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]

α : 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₂
⊢ μ[⇑(g₁ + g₂) * g|m] =ᶠ[ae μ] ⇑(g₁ + g₂) * μ[g|m]

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:
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 μ
s : Set α
c : ℝ
f : α → ℝ
⊢ s.indicator (Function.const α c) * f = s.indicator (c • f)

Tactic:
ext1 x

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

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:
refine (condExp_indicator (hg.smul c) hs).trans ?_

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:
α : 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|m] + μ[⇑g₂ * g|m]

Tactic:
rw [add_mul]

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)
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]

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

Tactic:
intro s c f

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

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:
refine condExp_congr_ae (EventuallyEq.mul ?_ EventuallyEq.rfl)

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)
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₂) =ᶠ[ae μ] ⇑g₁ + ⇑g₂