-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.lean
theorem condExp_restrict_ae_eq_restrict (hm : m ≤ m0) [SigmaFinite (μ.trim hm)]
    (hs_m : MeasurableSet[m] s) (hf_int : Integrable f μ) :
    (μ.restrict s)[f|m] =ᵐ[μ.restrict s] μ[f|m]

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 α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ⊤
⊢ ∫ (x : α) in t, s.indicator (μ.restrict s[f|m]) x ∂μ = ∫ (x : α) in t, s.indicator f x ∂μ

Tactic:
calc
  ∫ x in t, s.indicator ((μ.restrict s)[f|m]) x ∂μ =
      ∫ x in t, ((μ.restrict s)[f|m]) x ∂μ.restrict s := by
    rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m),
      Measure.restrict_restrict (hm _ ht), Set.inter_comm]
  _ = ∫ x in t, f x ∂μ.restrict s := setIntegral_condExp hm hf_int.integrableOn ht
  _ = ∫ x in t, s.indicator f x ∂μ := by
    rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m),
      Measure.restrict_restrict (hm _ ht), Set.inter_comm]

Result:
no goals

Proof state:
case refine_3
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
⊢ AEStronglyMeasurable (s.indicator (μ.restrict s[f|m])) μ

Tactic:
exact (stronglyMeasurable_condExp.indicator hs_m).aestronglyMeasurable

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 α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 < ⊤ → IntegrableOn (s.indicator (μ.restrict s[f|m])) s_1 μ

Tactic:
intro t ht _

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 α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ⊤
⊢ IntegrableOn (s.indicator (μ.restrict s[f|m])) t μ

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 α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
⊢ μ.restrict s[f|m] =ᶠ[ae (μ.restrict s)] μ[f|m]

Tactic:
have : SigmaFinite ((μ.restrict s).trim hm) := by rw [← restrict_trim hm _ hs_m]; infer_instance

Result:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
⊢ μ.restrict s[f|m] =ᶠ[ae (μ.restrict s)] μ[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 α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
⊢ s.indicator (μ.restrict s[f|m]) =ᶠ[ae μ] s.indicator (μ[f|m])

Tactic:
refine EventuallyEq.trans ?_ (condExp_indicator hf_int hs_m)

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

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 α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      μ s_1 < ⊤ → ∫ (x : α) in s_1, s.indicator (μ.restrict s[f|m]) x ∂μ = ∫ (x : α) in s_1, s.indicator f x ∂μ

Tactic:
intro t ht _

Result:
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 α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ⊤
⊢ ∫ (x : α) in t, s.indicator (μ.restrict s[f|m]) x ∂μ = ∫ (x : α) in t, s.indicator f 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 α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ⊤
⊢ ∫ (x : α) in t, s.indicator (μ.restrict s[f|m]) x ∂μ = ∫ (x : α) in t, (μ.restrict s[f|m]) x ∂μ.restrict s

Tactic:
rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m),
  Measure.restrict_restrict (hm _ ht), Set.inter_comm]

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 α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ⊤
h_int_restrict : Integrable (t.indicator (μ.restrict s[f|m])) (μ.restrict s)
⊢ Integrable (s.indicator (t.indicator (μ.restrict s[f|m]))) μ

Tactic:
rw [integrable_indicator_iff (hm _ hs_m), IntegrableOn]

Result:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ⊤
h_int_restrict : Integrable (t.indicator (μ.restrict s[f|m])) (μ.restrict s)
⊢ Integrable (t.indicator (μ.restrict s[f|m])) (μ.restrict s)