awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in t, s.indicator f x ∂μ)
have rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in s ∩ t, f x ∂μ)
Tactic: rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m),
          Measure.restrict_restrict (hm _ ht), Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in t, s.indicator f x ∂μ)
have rw₂ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t ∩ s, f x ∂μ) (∫ (x : α) in s ∩ t, f x ∂μ)
Tactic: rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m),
          Measure.restrict_restrict (hm _ ht), Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in t, s.indicator f x ∂μ)
have rw₃ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, f x ∂μ) (∫ (x : α) in s ∩ t, f x ∂μ)
Tactic: rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m),
          Measure.restrict_restrict (hm _ ht), Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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, s.indicator (μ.restrict s)[f | m] x ∂μ) (∫ (x : α) in t, s.indicator f x ∂μ)
have 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: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, s.indicator (μ.restrict s)[f | m] x ∂μ) (∫ (x : α) in t, s.indicator f x ∂μ)
have x₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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)
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] μ[f | m₂]
have rw : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]
Tactic: rw [ae_eq_restrict_iff_indicator_ae_eq (hm _ hs_m)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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
have rwa : MeasurableSet (s ∩ Set.univ)
Tactic: rwa [← Set.inter_univ s, ← hs Set.univ, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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)
⊢ MeasurableSet s
have rwa₁ : MeasurableSet (s ∩ Set.univ)
Tactic: rwa [← Set.inter_univ s, ← hs Set.univ, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (hypothesis)
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)
⊢ s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]
have hs_m₂ : MeasurableSet s
Tactic: have hs_m₂ : MeasurableSet[m₂] s := by rwa [← Set.inter_univ s, ← hs Set.univ, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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
⊢ s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]
have pos : ∀ (hf_int : Integrable f μ), s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]
Tactic: by_cases hf_int : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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₂]
⊢ s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]
have neg : ∀ (hf_int : ¬Integrable f μ), s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m₂]
Tactic: by_cases hf_int : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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₂]
have neg : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator 0) (s.indicator 0)
Tactic: simp_rw [condExp_of_not_integrable hf_int]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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₂]
have pos : μ[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₂)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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₂]
have 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 ∂μ)
Tactic: refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm₂
    (fun s _ _ => integrable_condExp.integrableOn)
    (fun s _ _ => integrable_condExp.integrableOn) ?_ ?_
    stronglyMeasurable_condExp.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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 ∂μ)
⊢ μ[s.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m₂]
have pos₁ : AEStronglyMeasurable μ[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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (hypothesis)
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 μ
⊢ AEStronglyMeasurable μ[s.indicator f | m] μ
have this : StronglyMeasurable μ[s.indicator f | m]
Tactic: have : StronglyMeasurable[m] (μ[s.indicator f | m]) := stronglyMeasurable_condExp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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] μ
have pos : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
Tactic: refine this.aestronglyMeasurable.of_measurableSpace_le_on hm hs_m (fun t => (hs t).mp) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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 ∂μ)
have 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 ∂μ
Tactic: rw [← integral_add_compl (hm _ hs_m) integrable_condExp.integrableOn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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
⊢ 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 ∂μ
have rw : HAdd.hAdd (α := E) (∫ (x : α) in s, μ[s.indicator f | m] x ∂μ.restrict t) 0 =
  ∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ
Tactic: rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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 ∂μ
⊢ 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 ∂μ
have 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 ∂μ)
Tactic: rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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 ∂μ)
⊢ 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 ∂μ
have rw₂ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ)
Tactic: rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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∞)
⊢ 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 ∂μ
have suffices : Eq.{u_2 + 1} (α := E) (∫ (x : α) in sᶜ, μ[s.indicator f | m] x ∂μ.restrict t) 0
Tactic: suffices ∫ x in sᶜ, (μ[s.indicator f | m]) x ∂μ.restrict t = 0 by
      rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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 sᶜ, μ[s.indicator f | m] x ∂μ.restrict t) 0
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : α) in sᶜ ∩ t, μ[s.indicator f | m] x ∂μ) 0
Tactic: rw [Measure.restrict_restrict (MeasurableSet.compl (hm _ hs_m))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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 sᶜ ∩ t, μ[s.indicator f | m] x ∂μ) 0
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ.restrict sᶜ) 0
Tactic: rw [Set.inter_comm, ← Measure.restrict_restrict (hm₂ _ ht)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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ᶜ)
have refine : ∀ᵐ (x : α) ∂μ.restrict sᶜ, x ∈ t → μ[s.indicator f | m] x = 0
Tactic: refine setIntegral_congr_ae (hm₂ _ ht) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
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 : α) ∂μ.restrict sᶜ, x ∈ t → μ[s.indicator f | m] x = 0
have 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
Tactic: filter_upwards [this] with x hx _ using hx