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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn.{u_1, u_2} (ε := E) 0 s_1 (μ.restrict s)

Tactic:
exact fun t _ _ => (integrable_zero _ _ _).integrableOn

Premises used: MeasureTheory.integrable_zero, 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
pos :
  LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[f | m] x ∂μ.restrict s) (∫ (x : α) in t, 0 x ∂μ.restrict s)
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[f | m] x ∂μ.restrict s) (∫ (x : α) in t, 0 x ∂μ.restrict s)

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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in t, 0 x ∂μ.restrict s)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[f | m] x ∂μ.restrict s) (∫ (x : α) in t, 0 x ∂μ.restrict s)

Tactic:
rw [Measure.restrict_restrict (hm _ ht), setIntegral_condExp hm hf_int (ht.inter hs), ←
      Measure.restrict_restrict (hm _ ht)]

Premises used: MeasureTheory.setIntegral_condExp, MeasureTheory.Measure.restrict_restrict, MeasurableSet.inter
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in t, 0 x ∂μ.restrict s)

Tactic:
setIntegral_congr_ae (hm _ ht) ?_

Premises used: MeasureTheory.setIntegral_congr_ae
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t → f x = 0 x
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in t, 0 x ∂μ.restrict s)

Tactic:
refine setIntegral_congr_ae (hm _ ht) ?_

Premises used: MeasureTheory.setIntegral_congr_ae
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h_1 : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : f x = 0 x
h : x ∈ t → f x = 0 x
⊢ x ∈ t → f x = 0 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : f x = 0 x
h_1 : x ∈ t
⊢ f x = 0 x

Tactic:
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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h_1 : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = 0 x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t → f x = 0 x) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : f x = 0 x), x ∈ t → f x = 0 x
⊢ ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t → f x = 0 x

Tactic:
filter_upwards [hf] with x hx _ using 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ AEStronglyMeasurable μ[f | m] (μ.restrict s)

Tactic:
stronglyMeasurable_condExp.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ AEStronglyMeasurable μ[f | m] (μ.restrict s)

Tactic:
exact stronglyMeasurable_condExp.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := E) 0 (μ.restrict s)

Tactic:
stronglyMeasurable_zero.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := E) 0 (μ.restrict s)

Tactic:
exact stronglyMeasurable_zero.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
pos : ∀ (hm : m ≤ m0), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
neg : ∀ (hm : ¬m ≤ m0), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]

Tactic:
by_cases hm : m ≤ m0
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : ¬m ≤ m0
neg : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]

Tactic:
simp_rw [condExp_of_not_le hm, Set.indicator_zero']

Premises used: MeasureTheory.condExp_of_not_le, Set.indicator_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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : ¬m ≤ m0
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0

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

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)
-- 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 α
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:
((hsf_zero (μ[f | m]) (condExp_ae_eq_restrict_zero hs.compl hf)).trans ?_).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_restrict_zero, MeasureTheory.condExp, MeasurableSet.compl, 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 α
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
pos : μ[f | m] =ᶠ[ae μ] μ[s.indicator f | m]
⊢ μ[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

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_restrict_zero, MeasureTheory.condExp, MeasurableSet.compl, 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 α
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:
condExp_congr_ae (hsf_zero f hf).symm

Premises used: MeasureTheory.condExp_congr_ae, 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 α
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

Premises used: MeasureTheory.condExp_congr_ae, 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
pos : ∀ (hm : m ≤ m0), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
neg : ∀ (hm : ¬m ≤ m0), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]

Tactic:
by_cases hm : m ≤ m0
-- 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
neg : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]

Tactic:
simp_rw [condExp_of_not_le hm, Set.indicator_zero']

Premises used: MeasureTheory.condExp_of_not_le, Set.indicator_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
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0

Tactic:
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
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.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 α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
neg : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm, Set.indicator_zero']

Premises used: Set.indicator_zero', MeasureTheory.condExp_of_not_sigmaFinite
-- 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 : ¬SigmaFinite (μ.trim hm)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0

Tactic:
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 : SigmaFinite (μ.trim hm)
⊢ SigmaFinite (μ.trim hm)

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

Tactic:
rw [Set.indicator_self_add_compl s f]

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

Tactic:
have : s.indicator (μ[f | m]) =ᵐ[μ] s.indicator (μ[s.indicator f + sᶜ.indicator f | m]) := by
    rw [Set.indicator_self_add_compl s f]
-- 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 | m] =ᶠ[ae μ] s.indicator μ[f | m]

Tactic:
(this.trans ?_).symm

Premises used: Filter.EventuallyEq.trans, 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]
pos : s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]

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

Premises used: Filter.EventuallyEq.trans, 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]
h :
  ∀ (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
⊢ 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

Premises used: MeasureTheory.condExp_add, MeasurableSet.compl, 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 α
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]
x : α
hx : μ[s.indicator f + sᶜ.indicator f | m] x = (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
h :
  (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
    s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
h₁ :
  (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
    if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0
h₂ h₃ :
  (if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0) =
    if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0
⊢ 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]

Premises used: Set.indicator_apply
-- 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]
x : α
hx : μ[s.indicator f + sᶜ.indicator f | m] x = (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
h :
  (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
    s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
h₁ :
  (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
    if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0
h₂ h₃ :
  (if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0) =
    if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] x = s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x

Tactic:
classical rw [Set.indicator_apply, Set.indicator_apply, hx]

Premises used: Set.indicator_apply
-- 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] + μ[sᶜ.indicator f | m]) =
    s.indicator μ[s.indicator f | m] + s.indicator μ[sᶜ.indicator f | m]

Tactic:
(s.indicator_add' _ _)

Premises used: Set.indicator_add'
-- 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] + s.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ]
    s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])

Tactic:
Filter.EventuallyEq.rfl.add ?_

Premises used: Filter.EventuallyEq.add, Filter.EventuallyEq.rfl