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 α
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 (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)
⊢ Integrable (s.indicator (t.indicator (μ.restrict s)[f | m])) μ

Tactic:
suffices h_int_restrict : Integrable (t.indicator ((μ.restrict s)[f | m])) (μ.restrict s) by
      rw [integrable_indicator_iff (hm _ hs_m), IntegrableOn]
      exact 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∞)
⊢ Integrable (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)

Tactic:
integrable_condExp.indicator (hm _ ht)

Premises used: 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
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)

Tactic:
exact integrable_condExp.indicator (hm _ ht)

Premises used: 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_2 :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, s.indicator (μ.restrict s)[f | m] x ∂μ) (∫ (x : α) in t, s.indicator f x ∂μ)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, s.indicator (μ.restrict s)[f | m] x ∂μ) (∫ (x : α) in t, s.indicator f x ∂μ)

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∞)
rw :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (μ.restrict s)[f | m] x ∂μ.restrict t)
    (∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s)
rw₁ :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, (μ.restrict s)[f | m] x ∂μ)
    (∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s)
rw₂ :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, (μ.restrict s)[f | m] x ∂μ)
    (∫ (x : α) in t ∩ s, (μ.restrict s)[f | m] x ∂μ)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in t ∩ s, (μ.restrict s)[f | m] x ∂μ)
    (∫ (x : α) in t ∩ s, (μ.restrict s)[f | m] x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (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]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.Measure.restrict_restrict, Set.inter_comm
-- 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∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s) (∫ (x : α) in t, f x ∂μ.restrict s)

Tactic:
setIntegral_condExp hm hf_int.integrableOn ht

Premises used: MeasureTheory.setIntegral_condExp, MeasureTheory.Integrable.integrableOn
-- 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∞)
rw : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in s, f x ∂μ.restrict t)
rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in s ∩ t, f x ∂μ)
rw₂ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t ∩ s, f x ∂μ) (∫ (x : α) in s ∩ t, f x ∂μ)
rw₃ rw₄ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, f x ∂μ) (∫ (x : α) in s ∩ t, f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in t, s.indicator f x ∂μ)

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

Premises used: MeasureTheory.integral_indicator, MeasureTheory.Measure.restrict_restrict, Set.inter_comm
-- 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∞)
x :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, s.indicator (μ.restrict s)[f | m] x ∂μ)
    (∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s)
x₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in t, s.indicator f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (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]

Premises used: MeasureTheory.setIntegral_condExp, MeasureTheory.Measure.restrict, MeasureTheory.Integrable.integrableOn
-- 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)
⊢ AEStronglyMeasurable (s.indicator (μ.restrict s)[f | m]) μ

Tactic:
(stronglyMeasurable_condExp.indicator hs_m).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.StronglyMeasurable.indicator, MeasureTheory.stronglyMeasurable_condExp
-- 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)
⊢ AEStronglyMeasurable (s.indicator (μ.restrict s)[f | m]) μ

Tactic:
exact (stronglyMeasurable_condExp.indicator hs_m).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.StronglyMeasurable.indicator, MeasureTheory.stronglyMeasurable_condExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
rw : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]
⊢ μ[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
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
rwa : MeasurableSet (s ∩ Set.univ)
rwa₁ : MeasurableSet (s ∩ Set.univ)
rwa₂ rwa₃ rwa₄ rwa₅ : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rwa [← Set.inter_univ s, ← hs Set.univ, Set.inter_univ]

Premises used: Set.univ, Set.inter_univ
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
⊢ MeasurableSet s

Tactic:
have hs_m₂ : MeasurableSet[m₂] s := by rwa [← Set.inter_univ s, ← hs Set.univ, Set.inter_univ]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
pos : ∀ (hf_int : Integrable f μ), s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]
neg : ∀ (hf_int : ¬Integrable f μ), s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]
⊢ s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]

Tactic:
by_cases hf_int : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : ¬Integrable f μ
neg : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator 0) (s.indicator 0)
⊢ s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]

Tactic:
simp_rw [condExp_of_not_integrable hf_int]

Premises used: MeasureTheory.condExp_of_not_integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : ¬Integrable f μ
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator 0) (s.indicator 0)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
⊢ s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]

Tactic:
((condExp_indicator hf_int hs_m).symm.trans ?_).trans (condExp_indicator hf_int hs_m₂)

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

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

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

Tactic:
ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm₂
    (fun s _ _ => integrable_condExp.integrableOn)
    (fun s _ _ => integrable_condExp.integrableOn) ?_ ?_
    stronglyMeasurable_condExp.aestronglyMeasurable

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.Integrable.integrableOn, MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
pos :
  ∀ (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 f | m] x ∂μ)
          (∫ (x : α) in s_1, μ[s.indicator f | m₂] x ∂μ)
pos₁ : AEStronglyMeasurable μ[s.indicator f | m] μ
⊢ μ[s.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m₂]

Tactic:
refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm₂
    (fun s _ _ => integrable_condExp.integrableOn)
    (fun s _ _ => integrable_condExp.integrableOn) ?_ ?_
    stronglyMeasurable_condExp.aestronglyMeasurable

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.Integrable.integrableOn, MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
⊢ StronglyMeasurable μ[s.indicator f | m]

Tactic:
have : StronglyMeasurable[m] (μ[s.indicator f | m]) := stronglyMeasurable_condExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
this : StronglyMeasurable μ[s.indicator f | m]
⊢ AEStronglyMeasurable μ[s.indicator f | m] μ

Tactic:
this.aestronglyMeasurable.of_measurableSpace_le_on hm hs_m (fun t => (hs t).mp) ?_

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.of_measurableSpace_le_on, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
this : StronglyMeasurable μ[s.indicator f | m]
pos : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ AEStronglyMeasurable μ[s.indicator f | m] μ

Tactic:
refine this.aestronglyMeasurable.of_measurableSpace_le_on hm hs_m (fun t => (hs t).mp) ?_

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.of_measurableSpace_le_on, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
this : StronglyMeasurable μ[s.indicator f | m]
⊢ μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0

Tactic:
condExp_ae_eq_restrict_zero hs_m.compl (indicator_ae_eq_restrict_compl (hm _ hs_m))

Premises used: MeasureTheory.condExp_ae_eq_restrict_zero, MeasurableSet.compl, indicator_ae_eq_restrict_compl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
this : StronglyMeasurable μ[s.indicator f | m]
⊢ μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0

Tactic:
exact condExp_ae_eq_restrict_zero hs_m.compl (indicator_ae_eq_restrict_compl (hm _ hs_m))

Premises used: MeasureTheory.condExp_ae_eq_restrict_zero, MeasurableSet.compl, indicator_ae_eq_restrict_compl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
pos :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HAdd.hAdd (α := E) (∫ (x : α) in s, μ[s.indicator f | m] x ∂μ.restrict t)
      (∫ (x : α) in sᶜ, μ[s.indicator f | m] x ∂μ.restrict t) =
    ∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ)

Tactic:
rw [← integral_add_compl (hm _ hs_m) integrable_condExp.integrableOn]

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.integral_add_compl, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Eq.{u_2 + 1} (α := E) (∫ (x : α) in sᶜ, μ[s.indicator f | m] x ∂μ.restrict t) 0
rw :
  HAdd.hAdd (α := E) (∫ (x : α) in s, μ[s.indicator f | m] x ∂μ.restrict t) 0 =
    ∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ
rw₁ :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, μ[s.indicator f | m] x ∂μ.restrict t)
    (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ)
⊢ HAdd.hAdd (α := E) (∫ (x : α) in s, μ[s.indicator f | m] x ∂μ.restrict t)
      (∫ (x : α) in sᶜ, μ[s.indicator f | m] x ∂μ.restrict t) =
    ∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ

Tactic:
rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]

Premises used: MeasureTheory.Measure.restrict_restrict, add_zero