-- 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:
α : 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 (μ[s.indicator f + sᶜ.indicator f|m])

Tactic:
rw [Set.indicator_self_add_compl s f]

Result:
no goals

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

Tactic:
exact indicator_ae_eq_restrict_compl (hm _ hs)

Result:
no goals

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 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
hxs : x ∈ s
⊢ s.indicator (μ[sᶜ.indicator f|m]) x = s.indicator (sᶜ.indicator (μ[sᶜ.indicator f|m])) x

Tactic:
simp only [hx, hxs, Set.indicator_of_mem]

Result:
no goals

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
⊢ 0 =ᶠ[ae μ] 0

Tactic:
rfl

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])
⊢ s.indicator (μ[s.indicator f|m]) + s.indicator (sᶜ.indicator (μ[sᶜ.indicator f|m])) =ᶠ[ae μ]
    s.indicator (μ[s.indicator f|m])

Tactic:
rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]

Result:
no goals

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 this✝ : SigmaFinite (μ.trim hm)
this : s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m])
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

Tactic:
refine (this.trans ?_).symm

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)
this : s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m])
⊢ s.indicator (μ[s.indicator f + sᶜ.indicator f|m]) =ᶠ[ae μ] μ[s.indicator f|m]

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:
rw [Set.indicator_apply, Set.indicator_apply, hx]

Result:
no goals

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

Tactic:
by_cases hxs : x ∈ s

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)
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
hxs : x ∈ s
⊢ s.indicator (μ[sᶜ.indicator f|m]) x = s.indicator (sᶜ.indicator (μ[sᶜ.indicator f|m])) x

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 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
hxs : x ∉ s
⊢ 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
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 + sᶜ.indicator f|m]) =ᶠ[ae μ] s.indicator (μ[s.indicator f|m] + μ[sᶜ.indicator f|m])

Tactic:
filter_upwards [condExp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl)) m]
  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])
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