awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inst : SigmaFinite (μ.trim hm)
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk
          (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          h x =
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          x
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                                  (indicatorConstLp (s := s) 2 hs hμs 1)) :
                              ↥(Lp ℝ 2 μ)) :
                          α →ₘ[μ] ℝ) :
                      α → ℝ)
                    x =
                  AEStronglyMeasurable.mk
                    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                                  (indicatorConstLp (s := s) 2 hs hμs 1)) :
                              ↥(Lp ℝ 2 μ)) :
                          α →ₘ[μ] ℝ) :
                      α → ℝ)
                    h x)
              x}
          x →
        Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                x ∈ t →
                  AEStronglyMeasurable.mk
                      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                                    (indicatorConstLp (s := s) 2 hs hμs 1)) :
                                ↥(Lp ℝ 2 μ)) :
                            α →ₘ[μ] ℝ) :
                        α → ℝ)
                      h x =
                    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                                    (indicatorConstLp (s := s) 2 hs hμs 1)) :
                                ↥(Lp ℝ 2 μ)) :
                            α →ₘ[μ] ℝ) :
                        α → ℝ)
                      x)
              x}
          x}
    a
Tactic: filter_upwards [h.ae_eq_mk] with x hx using fun _ => hx.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inst : SigmaFinite (μ.trim hm)
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0
    (∫ (x : α) in t,
      AEStronglyMeasurable.mk
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        h x ∂μ)
have h_ae : ∀ᵐ (x : α) ∂μ,
  x ∈ t →
    AEStronglyMeasurable.mk
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        h x =
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        x
Tactic: have h_ae :
        ∀ᵐ x ∂μ, x ∈ t → h.mk _ x = (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) x := by
      filter_upwards [h.ae_eq_mk] with x hx using fun _ => hx.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inst : SigmaFinite (μ.trim hm)
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ae :
  ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk
          (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          h x =
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          x
⊢ LE.le (α := ℝ) 0
    (∫ (x : α) in t,
      AEStronglyMeasurable.mk
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        h x ∂μ)
have refine_2 : 0 ≤ μ.real (s ∩ t)
Tactic: rw [setIntegral_congr_ae (hm t ht) h_ae,
      setIntegral_condExpL2_indicator ht hs ((le_trim hm).trans_lt hμt).ne hμs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : NormedSpace ℝ E
inst_3 : IsOrderedModule ℝ E
inst_4 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx : 0 ≤ x
⊢ 0 ≤ᶠ[ae μ] (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] E) : α → E)
have refine : EventuallyLE.{u_1, u_10} (β := E) (ae μ) 0 fun (a : α) ↦
  HSMul.hSMul (α := ℝ)
    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ)) :
            α →ₘ[μ] ℝ) :
        α → ℝ)
      a)
    x
Tactic: refine EventuallyLE.trans_eq ?_ (condExpIndSMul_ae_eq_smul hm hs hμs x).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : NormedSpace ℝ E
inst_3 : IsOrderedModule ℝ E
inst_4 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx : 0 ≤ x
⊢ EventuallyLE.{u_1, u_10} (β := E) (ae μ) 0 fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x
have h : ∀ (a : α)
  (ha :
    LE.le (α := ℝ) (0 a)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)),
  0 a ≤
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x
Tactic: filter_upwards [condExpL2_indicator_nonneg hm hs hμs] with a ha
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have pos : ∀ (hm : m ≤ m0), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
Tactic: by_cases hm : m ≤ m0
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
pos : ∀ (hm : m ≤ m0), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have neg : ∀ (hm : ¬m ≤ m0), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
Tactic: by_cases hm : m ≤ m0
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : ¬m ≤ m0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have neg : EventuallyEq.{u_1, u_2} (β := E) (ae (μ.restrict s)) 0 0
Tactic: simp_rw [condExp_of_not_le hm]
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have neg : EventuallyEq.{u_1, u_2} (β := E) (ae (μ.restrict s)) 0 0
Tactic: simp_rw [condExp_of_not_sigmaFinite hm hμ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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ SigmaFinite ((μ.restrict s).trim hm)
have rw : SigmaFinite ((μ.trim hm).restrict s)
Tactic: rw [← restrict_trim hm _ hs]
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have this₁ : SigmaFinite ((μ.restrict s).trim hm)
Tactic: have : SigmaFinite ((μ.restrict s).trim hm) := by
    rw [← restrict_trim hm _ hs]
    exact Restrict.sigmaFinite _ s
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have pos : ∀ (hf_int : Integrable f μ), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
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
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
pos : ∀ (hf_int : Integrable f μ), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have neg : ∀ (hf_int : ¬Integrable f μ), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
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
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : ¬Integrable f μ
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have neg : EventuallyEq.{u_1, u_2} (β := E) (ae (μ.restrict s)) 0 0
Tactic: 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
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have pos : ∀ (s_1 : Set α),
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn μ[f | m] s_1 (μ.restrict s)
Tactic: refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm ?_ ?_ ?_ ?_ ?_
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
pos :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn μ[f | m] s_1 (μ.restrict s)
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have pos₁ : ∀ (s_1 : Set α),
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn.{u_1, u_2} (ε := E) 0 s_1 (μ.restrict s)
Tactic: refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm ?_ ?_ ?_ ?_ ?_
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
pos :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn μ[f | m] s_1 (μ.restrict s)
pos₁ :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn.{u_1, u_2} (ε := E) 0 s_1 (μ.restrict s)
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have pos₂ : ∀ (s_1 : Set α),
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq.{u_2 + 1} (α := E) (∫ (x : α) in s_1, μ[f | m] x ∂μ.restrict s) (∫ (x : α) in s_1, 0 x ∂μ.restrict s)
Tactic: refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm ?_ ?_ ?_ ?_ ?_
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
pos :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn μ[f | m] s_1 (μ.restrict s)
pos₁ :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn.{u_1, u_2} (ε := E) 0 s_1 (μ.restrict s)
pos₂ :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s_1, μ[f | m] x ∂μ.restrict s) (∫ (x : α) in s_1, 0 x ∂μ.restrict s)
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have pos₃ : AEStronglyMeasurable μ[f | m] (μ.restrict s)
Tactic: refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm ?_ ?_ ?_ ?_ ?_
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
pos :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn μ[f | m] s_1 (μ.restrict s)
pos₁ :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn.{u_1, u_2} (ε := E) 0 s_1 (μ.restrict s)
pos₂ :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s_1, μ[f | m] x ∂μ.restrict s) (∫ (x : α) in s_1, 0 x ∂μ.restrict s)
pos₃ : AEStronglyMeasurable μ[f | m] (μ.restrict s)
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0
have pos₄ : AEStronglyMeasurable.{u_1, u_2} (β := E) 0 (μ.restrict s)
Tactic: refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm ?_ ?_ ?_ ?_ ?_
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, μ[f | m] x ∂μ.restrict s) (∫ (x : α) in t, 0 x ∂μ.restrict s)
have pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in t, 0 x ∂μ.restrict s)
Tactic: rw [Measure.restrict_restrict (hm _ ht), setIntegral_condExp hm hf_int (ht.inter hs), ←
      Measure.restrict_restrict (hm _ ht)]
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ.restrict s) (∫ (x : α) in t, 0 x ∂μ.restrict s)
have pos : ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t → f x = 0 x
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
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t → f x = 0 x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = 0 x) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t → f x = 0 x) x} x}
    a
Tactic: filter_upwards [hf] with x hx _ using hx
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
h_1 : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = 0 x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t → f x = 0 x) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t → f x = 0 x
have h₁ : ∀ (a : α), f a = 0 a → a ∈ t → f a = 0 a
Tactic: filter_upwards [hf] with x hx _ using hx
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have pos : ∀ (hm : m ≤ m0), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
Tactic: by_cases hm : m ≤ m0
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
pos : ∀ (hm : m ≤ m0), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have neg : ∀ (hm : ¬m ≤ m0), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
Tactic: by_cases hm : m ≤ m0
-- 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 α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : ¬m ≤ m0
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have neg : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_le hm, Set.indicator_zero']