-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.lean
theorem condExp_indicator_aux (hs : MeasurableSet[m] s) (hf : f =ᵐ[μ.restrict sᶜ] 0) :
    μ[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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : m ≤ m0
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

Tactic:
have hsf_zero : ∀ g : α → E, g =ᵐ[μ.restrict sᶜ] 0 → s.indicator g =ᵐ[μ] g := fun g =>
  indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs)

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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : m ≤ m0
hsf_zero : ∀ (g : α → E), g =ᶠ[ae (μ.restrict sᶜ)] 0 → s.indicator g =ᶠ[ae μ] g
⊢ μ[s.indicator f|m] =ᶠ[ae μ] 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ μ[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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : ¬m ≤ m0
⊢ μ[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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : ¬m ≤ m0
⊢ 0 =ᶠ[ae μ] 0

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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : m ≤ m0
hsf_zero : ∀ (g : α → E), g =ᶠ[ae (μ.restrict sᶜ)] 0 → s.indicator g =ᶠ[ae μ] g
⊢ μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])

Tactic:
refine ((hsf_zero (μ[f|m]) (condExp_ae_eq_restrict_zero hs.compl hf)).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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : m ≤ m0
hsf_zero : ∀ (g : α → E), g =ᶠ[ae (μ.restrict sᶜ)] 0 → s.indicator g =ᶠ[ae μ] g
⊢ μ[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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : m ≤ m0
hsf_zero : ∀ (g : α → E), g =ᶠ[ae (μ.restrict sᶜ)] 0 → s.indicator g =ᶠ[ae μ] g
⊢ μ[f|m] =ᶠ[ae μ] μ[s.indicator f|m]

Tactic:
exact condExp_congr_ae (hsf_zero f hf).symm

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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : m ≤ m0
⊢ μ[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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : ¬m ≤ m0
⊢ 0 =ᶠ[ae μ] 0

Tactic:
rfl

Result:
no goals