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 α
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] =ᶠ[ae μ] μ[s.indicator f | m]
have refine_1 : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0
Tactic: refine (condExp_indicator_aux hs ?_).symm.trans ?_
-- 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 α
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]
refine_1 : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ s.indicator μ[s.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
have refine_2 : μ[s.indicator (s.indicator f) | m] =ᶠ[ae μ] μ[s.indicator f | m]
Tactic: refine (condExp_indicator_aux hs ?_).symm.trans ?_
-- 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 α
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] =ᶠ[ae μ] μ[s.indicator f | m]
have refine_2 : μ[(s ∩ s).indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
Tactic: rw [Set.indicator_indicator, Set.inter_self]
-- 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 α
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]
refine_2 : μ[(s ∩ s).indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
⊢ μ[s.indicator (s.indicator f) | m] =ᶠ[ae μ] μ[s.indicator f | m]
have refine_2₁ : μ[s.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
Tactic: rw [Set.indicator_indicator, Set.inter_self]
-- 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 α
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 + sᶜ.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
have f₁ : s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m])
Tactic: calc
    s.indicator (μ[s.indicator f + sᶜ.indicator f | m]) =ᵐ[μ]
        s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) := by
      filter_upwards [condExp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl)) m]
        with x hx
      classical rw [Set.indicator_apply, Set.indicator_apply, hx]
    _ = s.indicator (μ[s.indicator f | m]) + s.indicator (μ[sᶜ.indicator f | m]) :=
      (s.indicator_add' _ _)
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) +
        s.indicator (sᶜ.indicator (μ[sᶜ.indicator f | m])) := by
      refine Filter.EventuallyEq.rfl.add ?_
      have : sᶜ.indicator (μ[sᶜ.indicator f | m]) =ᵐ[μ] μ[sᶜ.indicator f | m] := by
        refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
        · exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
        · rw [Set.indicator_indicator, Set.inter_self]
      filter_upwards [this] with x hx
      by_cases hxs : x ∈ s
      · simp only [hx, hxs, Set.indicator_of_mem]
      · simp only [hxs, Set.indicator_of_notMem, not_false_iff]
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) := by
      rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
    _ =ᵐ[μ] μ[s.indicator f | m] := by
      refine (condExp_indicator_aux hs ?_).symm.trans ?_
      · exact indicator_ae_eq_restrict_compl (hm _ hs)
      · rw [Set.indicator_indicator, Set.inter_self]
-- 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 α
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]
f₁ :
  s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m])
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
have f₂ : 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: calc
    s.indicator (μ[s.indicator f + sᶜ.indicator f | m]) =ᵐ[μ]
        s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) := by
      filter_upwards [condExp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl)) m]
        with x hx
      classical rw [Set.indicator_apply, Set.indicator_apply, hx]
    _ = s.indicator (μ[s.indicator f | m]) + s.indicator (μ[sᶜ.indicator f | m]) :=
      (s.indicator_add' _ _)
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) +
        s.indicator (sᶜ.indicator (μ[sᶜ.indicator f | m])) := by
      refine Filter.EventuallyEq.rfl.add ?_
      have : sᶜ.indicator (μ[sᶜ.indicator f | m]) =ᵐ[μ] μ[sᶜ.indicator f | m] := by
        refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
        · exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
        · rw [Set.indicator_indicator, Set.inter_self]
      filter_upwards [this] with x hx
      by_cases hxs : x ∈ s
      · simp only [hx, hxs, Set.indicator_of_mem]
      · simp only [hxs, Set.indicator_of_notMem, not_false_iff]
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) := by
      rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
    _ =ᵐ[μ] μ[s.indicator f | m] := by
      refine (condExp_indicator_aux hs ?_).symm.trans ?_
      · exact indicator_ae_eq_restrict_compl (hm _ hs)
      · rw [Set.indicator_indicator, Set.inter_self]
-- 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 α
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]
f₁ :
  s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m])
f₂ :
  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])
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
have f₃ : s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) =ᶠ[ae μ]
  s.indicator μ[s.indicator f | m]
Tactic: calc
    s.indicator (μ[s.indicator f + sᶜ.indicator f | m]) =ᵐ[μ]
        s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) := by
      filter_upwards [condExp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl)) m]
        with x hx
      classical rw [Set.indicator_apply, Set.indicator_apply, hx]
    _ = s.indicator (μ[s.indicator f | m]) + s.indicator (μ[sᶜ.indicator f | m]) :=
      (s.indicator_add' _ _)
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) +
        s.indicator (sᶜ.indicator (μ[sᶜ.indicator f | m])) := by
      refine Filter.EventuallyEq.rfl.add ?_
      have : sᶜ.indicator (μ[sᶜ.indicator f | m]) =ᵐ[μ] μ[sᶜ.indicator f | m] := by
        refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
        · exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
        · rw [Set.indicator_indicator, Set.inter_self]
      filter_upwards [this] with x hx
      by_cases hxs : x ∈ s
      · simp only [hx, hxs, Set.indicator_of_mem]
      · simp only [hxs, Set.indicator_of_notMem, not_false_iff]
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) := by
      rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
    _ =ᵐ[μ] μ[s.indicator f | m] := by
      refine (condExp_indicator_aux hs ?_).symm.trans ?_
      · exact indicator_ae_eq_restrict_compl (hm _ hs)
      · rw [Set.indicator_indicator, Set.inter_self]
-- 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 α
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]
f₁ :
  s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m])
f₂ :
  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])
f₃ :
  s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) =ᶠ[ae μ]
    s.indicator μ[s.indicator f | m]
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
have f₄ : s.indicator μ[s.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
Tactic: calc
    s.indicator (μ[s.indicator f + sᶜ.indicator f | m]) =ᵐ[μ]
        s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) := by
      filter_upwards [condExp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl)) m]
        with x hx
      classical rw [Set.indicator_apply, Set.indicator_apply, hx]
    _ = s.indicator (μ[s.indicator f | m]) + s.indicator (μ[sᶜ.indicator f | m]) :=
      (s.indicator_add' _ _)
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) +
        s.indicator (sᶜ.indicator (μ[sᶜ.indicator f | m])) := by
      refine Filter.EventuallyEq.rfl.add ?_
      have : sᶜ.indicator (μ[sᶜ.indicator f | m]) =ᵐ[μ] μ[sᶜ.indicator f | m] := by
        refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
        · exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
        · rw [Set.indicator_indicator, Set.inter_self]
      filter_upwards [this] with x hx
      by_cases hxs : x ∈ s
      · simp only [hx, hxs, Set.indicator_of_mem]
      · simp only [hxs, Set.indicator_of_notMem, not_false_iff]
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) := by
      rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
    _ =ᵐ[μ] μ[s.indicator f | m] := by
      refine (condExp_indicator_aux hs ?_).symm.trans ?_
      · exact indicator_ae_eq_restrict_compl (hm _ hs)
      · rw [Set.indicator_indicator, Set.inter_self]
-- 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 μ
⊢ SigmaFinite ((μ.restrict s).trim hm)
have rw : SigmaFinite ((μ.trim hm).restrict s)
Tactic: rw [← restrict_trim hm _ hs_m]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (hypothesis)
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 μ
⊢ (μ.restrict s)[f | m] =ᶠ[ae (μ.restrict s)] μ[f | m]
have this : SigmaFinite ((μ.restrict s).trim hm)
Tactic: have : SigmaFinite ((μ.restrict s).trim hm) := by rw [← restrict_trim hm _ hs_m]; infer_instance
-- 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)
⊢ (μ.restrict s)[f | m] =ᶠ[ae (μ.restrict s)] μ[f | m]
have rw : s.indicator (μ.restrict s)[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
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)
⊢ s.indicator (μ.restrict s)[f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have refine : s.indicator (μ.restrict s)[f | m] =ᶠ[ae μ] μ[s.indicator f | m]
Tactic: refine EventuallyEq.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
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)
⊢ s.indicator (μ.restrict s)[f | m] =ᶠ[ae μ] μ[s.indicator f | m]
have refine_1 : ∀ (s_1 : Set α),
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (s.indicator (μ.restrict s)[f | m]) s_1 μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm (hf_int.indicator (hm _ hs_m)) ?_ ?_ ?_
-- 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)
refine_1 :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (s.indicator (μ.restrict s)[f | m]) s_1 μ
⊢ s.indicator (μ.restrict s)[f | m] =ᶠ[ae μ] μ[s.indicator f | m]
have refine_2 : ∀ (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 (μ.restrict s)[f | m] x ∂μ)
        (∫ (x : α) in s_1, s.indicator f x ∂μ)
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm (hf_int.indicator (hm _ hs_m)) ?_ ?_ ?_
-- 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)
refine_1 :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (s.indicator (μ.restrict s)[f | m]) s_1 μ
refine_2 :
  ∀ (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 (μ.restrict s)[f | m] x ∂μ)
          (∫ (x : α) in s_1, s.indicator f x ∂μ)
⊢ s.indicator (μ.restrict s)[f | m] =ᶠ[ae μ] μ[s.indicator f | m]
have refine_3 : AEStronglyMeasurable (s.indicator (μ.restrict s)[f | m]) μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm (hf_int.indicator (hm _ hs_m)) ?_ ?_ ?_
-- 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∞)
⊢ IntegrableOn (s.indicator (μ.restrict s)[f | m]) t μ
have refine_1 : Integrable (s.indicator (t.indicator (μ.restrict s)[f | m])) μ
Tactic: rw [← integrable_indicator_iff (hm _ ht), Set.indicator_indicator, Set.inter_comm, ←
      Set.indicator_indicator]
-- 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∞)
⊢ Integrable (s.indicator (t.indicator (μ.restrict s)[f | m])) μ
have refine_1 : Integrable (t.indicator (μ.restrict s)[f | m]) (μ.restrict s)
Tactic: suffices h_int_restrict : Integrable (t.indicator ((μ.restrict s)[f | m])) (μ.restrict s) by
      rw [integrable_indicator_iff (hm _ hs_m), IntegrableOn]
      exact h_int_restrict
-- 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, (μ.restrict s)[f | m] x ∂μ.restrict s)
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (μ.restrict s)[f | m] x ∂μ.restrict t)
  (∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s)
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 s, (μ.restrict s)[f | m] x ∂μ.restrict t)
    (∫ (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, (μ.restrict s)[f | m] x ∂μ.restrict s)
have rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, (μ.restrict s)[f | m] x ∂μ)
  (∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s)
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 s, (μ.restrict s)[f | m] x ∂μ.restrict t)
    (∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s)
rw₁ :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, (μ.restrict s)[f | m] x ∂μ)
    (∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s)
⊢ 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)
have rw₂ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, (μ.restrict s)[f | m] x ∂μ) (∫ (x : α) in t ∩ s, (μ.restrict s)[f | m] 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 s, (μ.restrict s)[f | m] x ∂μ.restrict t)
    (∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s)
rw₁ :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, (μ.restrict s)[f | m] x ∂μ)
    (∫ (x : α) in t, (μ.restrict s)[f | m] x ∂μ.restrict s)
rw₂ :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, (μ.restrict s)[f | m] x ∂μ)
    (∫ (x : α) in t ∩ s, (μ.restrict s)[f | m] x ∂μ)
⊢ 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)
have rw₃ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t ∩ s, (μ.restrict s)[f | m] x ∂μ) (∫ (x : α) in t ∩ s, (μ.restrict s)[f | m] 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, 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, f x ∂μ.restrict t)
Tactic: rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m),
          Measure.restrict_restrict (hm _ ht), Set.inter_comm]