-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.lean
theorem condExp_indicator (hf_int : Integrable f μ) (hs : MeasurableSet[m] s) :
    μ[s.indicator f|m] =ᵐ[μ] s.indicator (μ[f|m])

Proof state:
case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : ¬m ≤ m0
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

Tactic:
swap

Result:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : ¬m ≤ m0
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

Proof state:
case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

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

Result:
case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

Proof state:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm, Set.indicator_zero']

Result:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᶠ[ae μ] 0

Proof state:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m])
⊢ s.indicator (μ[s.indicator f|m]) =ᶠ[ae μ] μ[s.indicator f|m]

Tactic:
refine (condExp_indicator_aux hs ?_).symm.trans ?_

Result:
case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m])
⊢ s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0

case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m])
⊢ μ[s.indicator (s.indicator f)|m] =ᶠ[ae μ] μ[s.indicator f|m]

Proof state:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : ¬m ≤ m0
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

Tactic:
simp_rw [condExp_of_not_le hm, Set.indicator_zero']

Result:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : ¬m ≤ m0
⊢ 0 =ᶠ[ae μ] 0

Proof state:
case h
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m])
x : α
hx : (μ[s.indicator f + sᶜ.indicator f|m]) x = (μ[s.indicator f|m] + μ[sᶜ.indicator f|m]) x
⊢ s.indicator (μ[s.indicator f + sᶜ.indicator f|m]) x = s.indicator (μ[s.indicator f|m] + μ[sᶜ.indicator f|m]) x

Tactic:
classical rw [Set.indicator_apply, Set.indicator_apply, hx]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m])
⊢ μ[sᶜ.indicator (sᶜ.indicator f)|m] =ᶠ[ae μ] μ[sᶜ.indicator f|m]

Tactic:
rw [Set.indicator_indicator, Set.inter_self]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝¹ : SigmaFinite (μ.trim hm)
this✝ : s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m])
this : sᶜ.indicator (μ[sᶜ.indicator f|m]) =ᶠ[ae μ] μ[sᶜ.indicator f|m]
⊢ s.indicator (μ[sᶜ.indicator f|m]) =ᶠ[ae μ] s.indicator (sᶜ.indicator (μ[sᶜ.indicator f|m]))

Tactic:
filter_upwards [this] with x hx

Result:
case h
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝¹ : SigmaFinite (μ.trim hm)
this✝ : s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m])
this : sᶜ.indicator (μ[sᶜ.indicator f|m]) =ᶠ[ae μ] μ[sᶜ.indicator f|m]
x : α
hx : sᶜ.indicator (μ[sᶜ.indicator f|m]) x = (μ[sᶜ.indicator f|m]) x
⊢ s.indicator (μ[sᶜ.indicator f|m]) x = s.indicator (sᶜ.indicator (μ[sᶜ.indicator f|m])) x

Proof state:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

Tactic:
by_cases hm : m ≤ m0

Result:
case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : ¬m ≤ m0
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])