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
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
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ, x ∈ t → μ[s.indicator f | m] x = 0
have h₁ : ∀ (a : α), μ[s.indicator f | m] a = 0 a → a ∈ t → μ[s.indicator f | m] a = 0
Tactic: filter_upwards [this] with x hx _ using hx
-- 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ᶜ) 0
have x : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ.restrict sᶜ) (∫ (x : α) in t, 0 ∂μ.restrict sᶜ)
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 _ _
-- 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ᶜ ∩ t, μ[s.indicator f | m] x ∂μ) 0
have suffices : μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 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 _ _
-- 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∞)
⊢ μ[s.indicator f | m] =ᶠ[ae (μ.restrict sᶜ)] 0
have refine : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0
Tactic: refine condExp_ae_eq_restrict_zero hs_m.compl ?_
-- 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 μ
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 t, μ[s.indicator f | m₂] x ∂μ)
have this : 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)
-- 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 μ
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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)
have hst_m : MeasurableSet (s ∩ t)
Tactic: have hst_m : MeasurableSet[m] (s ∩ t) := (hs _).mpr (hs_m₂.inter 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 : 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)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)
have pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ 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]
-- 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 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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)
have pos₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, s.indicator f 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]
-- 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 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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)
have pos₂ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, s.indicator f x ∂μ) (∫ (x : α) in t, s.indicator f 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]
-- 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 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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)
have pos₃ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ.restrict (s ∩ t)) (∫ (x : α) in s, f x ∂μ.restrict t)
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]
-- 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 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)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)
have pos₄ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ (s ∩ t), f x ∂μ) (∫ (x : α) in s ∩ t, f 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]
-- 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 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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[s.indicator f | m] x ∂μ) (∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ)
have pos₅ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ s ∩ t, f x ∂μ) (∫ (x : α) in s ∩ t, f 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
have pos : ∀ (hm : m ≤ m𝓧), (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
Tactic: by_cases hm : m ≤ m𝓧
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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]
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
have neg : ∀ (hm : ¬m ≤ m𝓧), (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
Tactic: by_cases hm : m ≤ m𝓧
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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 : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
have neg : (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ 0) fun (x : 𝓧) ↦ 0
Tactic: simp [condLExp_of_not_le hm, condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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 : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
have pos : ∀ (hμ : SigmaFinite (μ.trim hm)),
  (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
Tactic: by_cases hμ : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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]
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
have neg : ∀ (hμ : ¬SigmaFinite (μ.trim hm)),
  (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
Tactic: by_cases hμ : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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]
have neg : (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ 0) fun (x : 𝓧) ↦ 0
Tactic: simp [condLExp_of_not_sigmaFinite hm hμ, condExp_of_not_sigmaFinite hm hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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]
have pos : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ (f x).toReal) μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm (E := ℝ) ?_ ?_ ?_ ?_ (μ := μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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) μ
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
have pos₁ : ∀ (s : Set 𝓧),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (ε := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) s μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm (E := ℝ) ?_ ?_ ?_ ?_ (μ := μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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 μ
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
have 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 ∂μ)
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm (E := ℝ) ?_ ?_ ?_ ?_ (μ := μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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 ∂μ)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ[fun (x : 𝓧) ↦ (f x).toReal | m]
have pos₃ : AEStronglyMeasurable (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm (E := ℝ) ?_ ?_ ?_ ?_ (μ := μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ (f x).toReal) μ
have pos : ∀ᵐ (x : 𝓧) ∂μ, f x ≠ ∞
Tactic: rwa [integrable_toReal_iff (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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 : 𝓧) ∂μ, f x ≠ ∞
have 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
Tactic: filter_upwards [ae_lt_top' (by fun_prop) hf] with x hx using hx.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
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
⊢ ∀ᵐ (x : 𝓧) ∂μ, f x ≠ ∞
have h₁ : ∀ (a : 𝓧), f a < ∞ → f a ≠ ∞
Tactic: filter_upwards [ae_lt_top' (by fun_prop) hf] with x hx using hx.ne