awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞)
suffices : Eq.{u_2 + 1} (α := E) (∫ (x : α) in sᶜ, μ[s.indicator f | m] x ∂μ.restrict t) 0
⊢ 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:
suffices ∫ x in sᶜ, (μ[s.indicator f | m]) x ∂μ.restrict t = 0 by
      rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
-- 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 : Eq.{u_2 + 1} (α := E) (∫ (x : α) in sᶜ ∩ t, μ[s.indicator f | m] x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in sᶜ, μ[s.indicator f | m] x ∂μ.restrict t) 0

Tactic:
rw [Measure.restrict_restrict (MeasurableSet.compl (hm _ hs_m))]

Premises used: MeasureTheory.Measure.restrict_restrict, MeasurableSet.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
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
rw : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ.restrict sᶜ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in sᶜ ∩ t, μ[s.indicator f | m] x ∂μ) 0

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

Premises used: MeasureTheory.Measure.restrict_restrict, Set.inter_comm
-- 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 : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ.restrict sᶜ) (∫ (x : α) in t, 0 ∂μ.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
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 : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
refine : ∀ᵐ (x : α) ∂μ.restrict sᶜ, x ∈ t → μ[s.indicator f | m] x = 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ.restrict sᶜ) (∫ (x : α) in t, 0 ∂μ.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
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_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : μ[s.indicator f | m] x = 0 x
h : x ∈ t → μ[s.indicator f | m] x = 0
⊢ x ∈ t → μ[s.indicator f | m] x = 0

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∞)
this : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : μ[s.indicator f | m] x = 0 x
h_1 : x ∈ t
⊢ μ[s.indicator f | m] x = 0

Tactic:
hx
-- 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_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ[s.indicator f | m] x = 0 x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t → μ[s.indicator f | m] x = 0) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : μ[s.indicator f | m] x = 0 x), x ∈ t → μ[s.indicator f | m] x = 0
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ, x ∈ t → μ[s.indicator f | m] x = 0

Tactic:
filter_upwards [this] with x hx _ using hx
-- 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 : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, 0 ∂μ.restrict sᶜ) 0

Tactic:
integral_zero _ _

Premises used: MeasureTheory.integral_zero
-- 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 : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
x : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ.restrict sᶜ) (∫ (x : α) in t, 0 ∂μ.restrict sᶜ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ.restrict sᶜ) 0

Tactic:
calc
        ∫ x : α in t, (μ[s.indicator f | m]) x ∂μ.restrict sᶜ =
            ∫ x : α in t, 0 ∂μ.restrict sᶜ := by
          refine setIntegral_congr_ae (hm₂ _ ht) ?_
          filter_upwards [this] with x hx _ using hx
        _ = 0 := integral_zero _ _

Premises used: Compl.compl, MeasureTheory.Measure.restrict, MeasureTheory.integral_zero
-- 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∞)
suffices : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in sᶜ ∩ t, μ[s.indicator f | m] x ∂μ) 0

Tactic:
suffices μ[s.indicator f | m] =ᵐ[μ.restrict sᶜ] 0 by
      rw [Set.inter_comm, ← Measure.restrict_restrict (hm₂ _ ht)]
      calc
        ∫ x : α in t, (μ[s.indicator f | m]) x ∂μ.restrict sᶜ =
            ∫ x : α in t, 0 ∂μ.restrict sᶜ := by
          refine setIntegral_congr_ae (hm₂ _ ht) ?_
          filter_upwards [this] with x hx _ using hx
        _ = 0 := integral_zero _ _
-- 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∞)
⊢ μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0

Tactic:
condExp_ae_eq_restrict_zero hs_m.compl ?_

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

Tactic:
refine condExp_ae_eq_restrict_zero hs_m.compl ?_

Premises used: MeasureTheory.condExp_ae_eq_restrict_zero, MeasurableSet.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
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0

Tactic:
indicator_ae_eq_restrict_compl (hm _ hs_m)

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

Tactic:
exact indicator_ae_eq_restrict_compl (hm _ hs_m)

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

Tactic:
have : ∫ x in t, (μ[s.indicator f | m]) x ∂μ = ∫ x in s ∩ t, (μ[s.indicator f | m]) x ∂μ := by
    rw [← integral_add_compl (hm _ hs_m) integrable_condExp.integrableOn]
    suffices ∫ x in sᶜ, (μ[s.indicator f | m]) x ∂μ.restrict t = 0 by
      rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
    rw [Measure.restrict_restrict (MeasurableSet.compl (hm _ hs_m))]
    suffices μ[s.indicator f | m] =ᵐ[μ.restrict sᶜ] 0 by
      rw [Set.inter_comm, ← Measure.restrict_restrict (hm₂ _ ht)]
      calc
        ∫ x : α in t, (μ[s.indicator f | m]) x ∂μ.restrict sᶜ =
            ∫ x : α in t, 0 ∂μ.restrict sᶜ := by
          refine setIntegral_congr_ae (hm₂ _ ht) ?_
          filter_upwards [this] with x hx _ using hx
        _ = 0 := integral_zero _ _
    refine condExp_ae_eq_restrict_zero hs_m.compl ?_
    exact indicator_ae_eq_restrict_compl (hm _ hs_m)
-- 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 t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ)
⊢ MeasurableSet (s ∩ t)

Tactic:
have hst_m : MeasurableSet[m] (s ∩ t) := (hs _).mpr (hs_m₂.inter ht)
-- 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 t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ)
hst_m : MeasurableSet (s ∩ t)
pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)
pos₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, s.indicator f x ∂μ)
pos₂ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, s.indicator f x ∂μ) (∫ (x : α) in t, s.indicator f x ∂μ)
pos₃ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ.restrict (s ∩ t)) (∫ (x : α) in s, f x ∂μ.restrict t)
pos₄ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ (s ∩ t), f x ∂μ) (∫ (x : α) in s ∩ t, f x ∂μ)
pos₅ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ s ∩ t, f x ∂μ) (∫ (x : α) in s ∩ t, f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)

Tactic:
simp_rw [this, setIntegral_condExp hm₂ (hf_int.indicator (hm _ hs_m)) ht,
    setIntegral_condExp hm (hf_int.indicator (hm _ hs_m)) hst_m, integral_indicator (hm _ hs_m),
    Measure.restrict_restrict (hm _ hs_m), ← Set.inter_assoc, Set.inter_self]

Premises used: MeasureTheory.setIntegral_condExp, MeasureTheory.integral_indicator, Set.inter_self, MeasureTheory.Measure.restrict_restrict, Set.inter_assoc, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
pos : ∀ (hm : m ≤ m𝓧), (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
neg :
  ∀ (hm : ¬m ≤ m𝓧), (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]

Tactic:
by_cases hm : m ≤ m𝓧
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : ¬m ≤ m𝓧
neg : (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ 0) fun (x : 𝓧) ↦ 0
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]

Tactic:
simp [condLExp_of_not_le hm, condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le, MeasureTheory.condLExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : ¬m ≤ m𝓧
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ 0) fun (x : 𝓧) ↦ 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
pos :
  ∀ (hμ : SigmaFinite (μ.trim hm)),
    (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
neg :
  ∀ (hμ : ¬SigmaFinite (μ.trim hm)),
    (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]

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

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : ¬SigmaFinite (μ.trim hm)
neg : (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ 0) fun (x : 𝓧) ↦ 0
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]

Tactic:
simp [condLExp_of_not_sigmaFinite hm hμ, condExp_of_not_sigmaFinite hm hμ]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite, MeasureTheory.condLExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : ¬SigmaFinite (μ.trim hm)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ 0) fun (x : 𝓧) ↦ 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]

Tactic:
ae_eq_condExp_of_forall_setIntegral_eq hm (E := ℝ) ?_ ?_ ?_ ?_ (μ := μ)

Premises used: MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
pos : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ (f x).toReal) μ
pos₁ :
  ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) s μ
pos₂ :
  ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : 𝓧) in s, (μ⁻[f|m] x).toReal ∂μ) (∫ (x : 𝓧) in s, (f x).toReal ∂μ)
pos₃ : AEStronglyMeasurable (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq hm (E := ℝ) ?_ ?_ ?_ ?_ (μ := μ)

Premises used: MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
⊢ AEMeasurable f μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
pos : ∀ᵐ (x : 𝓧) ∂μ, f x ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ (f x).toReal) μ

Tactic:
rwa [integrable_toReal_iff (by fun_prop)]

Premises used: MeasureTheory.integrable_toReal_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
x : 𝓧
hx : f x < ∞
⊢ f x ≠ ∞

Tactic:
hx.ne

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
h :
  ∀ (a : 𝓧),
    Membership.mem (γ := Set 𝓧)
      {x : 𝓧 |
        Membership.mem (γ := Set 𝓧) {x : 𝓧 | (fun (x : 𝓧) ↦ f x < ∞) x} x →
          Membership.mem (γ := Set 𝓧) {x : 𝓧 | (fun (x : 𝓧) ↦ f x ≠ ∞) x} x}
      a
h₁ h₂ : ∀ (x : 𝓧) (hx : f x < ∞), f x ≠ ∞
⊢ ∀ᵐ (x : 𝓧) ∂μ, f x ≠ ∞

Tactic:
filter_upwards [ae_lt_top' (by fun_prop) hf] with x hx using hx.ne

Premises used: MeasureTheory.ae_lt_top'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
⊢ ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) s μ

Tactic:
fun s hs hsμ ↦ Integrable.integrableOn ?_

Premises used: MeasureTheory.Integrable.integrableOn