awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
refine : s.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])
⊢ s.indicator μ[s.indicator f | m] + s.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ]
    s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])

Tactic:
refine Filter.EventuallyEq.rfl.add ?_

Premises used: Filter.EventuallyEq.add, Filter.EventuallyEq.rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : 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:
(condExp_indicator_aux hs.compl ?_).symm.trans ?_

Premises used: Filter.EventuallyEq.trans, MeasurableSet.compl, MeasureTheory.condExp_indicator_aux, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
refine_1 : sᶜ.indicator f =ᶠ[ae (μ.restrict sᶜᶜ)] 0
refine_2 : μ[sᶜ.indicator (sᶜ.indicator f) | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
⊢ sᶜ.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]

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

Premises used: Filter.EventuallyEq.trans, MeasurableSet.compl, MeasureTheory.condExp_indicator_aux, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : 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:
indicator_ae_eq_restrict_compl (hm _ hs.compl)

Premises used: MeasurableSet.compl, indicator_ae_eq_restrict_compl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : 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.compl)

Premises used: MeasurableSet.compl, indicator_ae_eq_restrict_compl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
refine_2 : μ[(sᶜ ∩ sᶜ).indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
refine_2₁ refine_2₂ : μ[sᶜ.indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
⊢ μ[sᶜ.indicator (sᶜ.indicator f) | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]

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

Premises used: Set.inter_self, Set.indicator_indicator
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : 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:
have : sᶜ.indicator (μ[sᶜ.indicator f | m]) =ᵐ[μ] μ[sᶜ.indicator f | m] := by
        refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
        · exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
        · rw [Set.indicator_indicator, Set.inter_self]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this_2 : 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]
h :
  ∀ (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
⊢ s.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])

Tactic:
filter_upwards [this] with x hx
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this_2 : 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
pos : ∀ (hxs : x ∈ s), s.indicator μ[sᶜ.indicator f | m] x = s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) x
neg : ∀ (hxs : x ∉ s), s.indicator μ[sᶜ.indicator f | m] x = s.indicator (sᶜ.indicator μ[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
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this_2 : 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]

Premises used: Set.indicator_of_mem
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this_2 : 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 [hxs, Set.indicator_of_notMem, not_false_iff]

Premises used: Set.indicator_of_notMem, not_false_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
rw :
  s.indicator μ[s.indicator f | m] + (s ∩ sᶜ).indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
rw₁ : s.indicator μ[s.indicator f | m] + Set.indicator ∅ μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
rw₂ : s.indicator μ[s.indicator f | m] + 0 =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
rw₃ rw₄ : s.indicator μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[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]

Premises used: Set.indicator_empty', Set.indicator_indicator, Set.inter_compl_self, add_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : 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:
(condExp_indicator_aux hs ?_).symm.trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_indicator_aux, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
refine_1 : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0
refine_2 : μ[s.indicator (s.indicator f) | m] =ᶠ[ae μ] μ[s.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]

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

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_indicator_aux, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : 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:
indicator_ae_eq_restrict_compl (hm _ hs)

Premises used: indicator_ae_eq_restrict_compl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : 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)

Premises used: indicator_ae_eq_restrict_compl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
refine_2 : μ[(s ∩ s).indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
refine_2₁ refine_2₂ : μ[s.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
⊢ μ[s.indicator (s.indicator f) | m] =ᶠ[ae μ] μ[s.indicator f | m]

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

Premises used: Set.inter_self, Set.indicator_indicator
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
f₁ :
  s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m])
f₂ :
  s.indicator μ[s.indicator f | m] + s.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ]
    s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])
f₃ :
  s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) =ᶠ[ae μ]
    s.indicator μ[s.indicator f | m]
f₄ : s.indicator μ[s.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]

Tactic:
calc
    s.indicator (μ[s.indicator f + sᶜ.indicator f | m]) =ᵐ[μ]
        s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) := by
      filter_upwards [condExp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl)) m]
        with x hx
      classical rw [Set.indicator_apply, Set.indicator_apply, hx]
    _ = s.indicator (μ[s.indicator f | m]) + s.indicator (μ[sᶜ.indicator f | m]) :=
      (s.indicator_add' _ _)
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) +
        s.indicator (sᶜ.indicator (μ[sᶜ.indicator f | m])) := by
      refine Filter.EventuallyEq.rfl.add ?_
      have : sᶜ.indicator (μ[sᶜ.indicator f | m]) =ᵐ[μ] μ[sᶜ.indicator f | m] := by
        refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
        · exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
        · rw [Set.indicator_indicator, Set.inter_self]
      filter_upwards [this] with x hx
      by_cases hxs : x ∈ s
      · simp only [hx, hxs, Set.indicator_of_mem]
      · simp only [hxs, Set.indicator_of_notMem, not_false_iff]
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) := by
      rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
    _ =ᵐ[μ] μ[s.indicator f | m] := by
      refine (condExp_indicator_aux hs ?_).symm.trans ?_
      · exact indicator_ae_eq_restrict_compl (hm _ hs)
      · rw [Set.indicator_indicator, Set.inter_self]

Premises used: Set.indicator, Compl.compl, Set.indicator_add', MeasureTheory.condExp, HAdd.hAdd
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
rw : SigmaFinite ((μ.trim hm).restrict s)
⊢ SigmaFinite ((μ.restrict s).trim hm)

Tactic:
rw [← restrict_trim hm _ hs_m]

Premises used: MeasureTheory.restrict_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
⊢ SigmaFinite ((μ.trim hm).restrict s)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
⊢ SigmaFinite ((μ.restrict s).trim hm)

Tactic:
have : SigmaFinite ((μ.restrict s).trim hm) := by rw [← restrict_trim hm _ hs_m]; infer_instance
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
rw : s.indicator (μ.restrict s)[f | m] =ᶠ[ae μ] s.indicator μ[f | m]
⊢ (μ.restrict s)[f | m] =ᶠ[ae (μ.restrict s)] μ[f | m]

Tactic:
rw [ae_eq_restrict_iff_indicator_ae_eq (hm _ hs_m)]

Premises used: ae_eq_restrict_iff_indicator_ae_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : 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:
EventuallyEq.trans ?_ (condExp_indicator hf_int hs_m)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_indicator
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
refine : s.indicator (μ.restrict s)[f | m] =ᶠ[ae μ] μ[s.indicator f | m]
⊢ s.indicator (μ.restrict s)[f | m] =ᶠ[ae μ] s.indicator μ[f | m]

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

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_indicator
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : 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:
ae_eq_condExp_of_forall_setIntegral_eq hm (hf_int.indicator (hm _ hs_m)) ?_ ?_ ?_

Premises used: MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
refine_1 :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (s.indicator (μ.restrict s)[f | m]) s_1 μ
refine_2 :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s_1, s.indicator (μ.restrict s)[f | m] x ∂μ)
          (∫ (x : α) in s_1, s.indicator f x ∂μ)
refine_3 : AEStronglyMeasurable (s.indicator (μ.restrict s)[f | m]) μ
⊢ s.indicator (μ.restrict s)[f | m] =ᶠ[ae μ] μ[s.indicator f | m]

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq hm (hf_int.indicator (hm _ hs_m)) ?_ ?_ ?_

Premises used: MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
refine_1 :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    IntegrableOn (s.indicator (μ.restrict s)[f | m]) t μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    IntegrableOn (s.indicator (μ.restrict s)[f | m]) t μ

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : Integrable (s.indicator (t.indicator (μ.restrict s)[f | m])) μ
⊢ IntegrableOn (s.indicator (μ.restrict s)[f | m]) t μ

Tactic:
rw [← integrable_indicator_iff (hm _ ht), Set.indicator_indicator, Set.inter_comm, ←
      Set.indicator_indicator]

Premises used: Set.inter_comm, Set.indicator_indicator, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_int_restrict : Integrable (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)
rw : 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]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_int_restrict : Integrable (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)
⊢ Integrable (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)

Tactic:
h_int_restrict
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_int_restrict : Integrable (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)
⊢ Integrable (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)

Tactic:
exact h_int_restrict