awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f_1 : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
hg :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      HAdd.hAdd (α := α → F') (β := α → F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
have refine_2 : Eq.{u_3 + 1} (α := F')
  (∫ (x : α) in s,
    HAdd.hAdd (α := α → F') (β := α → F')
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
      x ∂μ)
  (∫ (x : α) in s,
    ((↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F')) x ∂μ)
Tactic: rw [setIntegral_congr_ae (hm s hs)
      ((Lp.coeFn_add (hf_Lp.toLp f) (hg_Lp.toLp g)).mono fun x hx _ => hx)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f_1 : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
hg :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      HAdd.hAdd (α := α → F') (β := α → F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s,
      ((↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F')) x ∂μ)
have refine_2 : Eq.{u_3 + 1} (α := F')
  (∫ (x : α) in s,
    HAdd.hAdd (α := F')
      ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F') x)
      ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x) ∂μ)
  (∫ (x : α) in s,
    (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
Tactic: simp_rw [Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f_1 : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
hg :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      HAdd.hAdd (α := F')
        ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
          x)
        ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          x) ∂μ)
    (∫ (x : α) in s,
      (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
have refine_2 : HAdd.hAdd (α := F')
    (∫ (a : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        a ∂μ)
    (∫ (a : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        a ∂μ) =
  ∫ (x : α) in s,
    (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ
Tactic: rw [integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn,
      integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn, hf,
      hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f_1 : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
hg :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
refine_2 :
  HAdd.hAdd (α := F')
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ)
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ) =
    ∫ (x : α) in s,
      (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      HAdd.hAdd (α := F')
        ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
          x)
        ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          x) ∂μ)
    (∫ (x : α) in s,
      (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
have refine_2₁ : HAdd.hAdd (α := F')
    (∫ (a : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        a ∂μ)
    (∫ (a : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        a ∂μ) =
  HAdd.hAdd (α := F') (∫ (a : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
    (∫ (a : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
Tactic: rw [integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn,
      integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn, hf,
      hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f_1 : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
hg :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
refine_2 :
  HAdd.hAdd (α := F')
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ)
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ) =
    ∫ (x : α) in s,
      (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ
refine_2₁ :
  HAdd.hAdd (α := F')
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ)
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ) =
    HAdd.hAdd (α := F') (∫ (a : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
      (∫ (a : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      HAdd.hAdd (α := F')
        ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
          x)
        ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          x) ∂μ)
    (∫ (x : α) in s,
      (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
have refine_2₂ : HAdd.hAdd (α := F') (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (a : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        a ∂μ) =
  HAdd.hAdd (α := F') (∫ (a : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
    (∫ (a : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
Tactic: rw [integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn,
      integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn, hf,
      hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
Tactic: have hS_meas : ∀ i, MeasurableSet[m] (S i) := measurableSet_spanningSets (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
Tactic: have hS_meas0 : ∀ i, MeasurableSet (S i) := fun i => hm _ (hS_meas i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
⊢ s = ⋃ (i : ℕ), S i ∩ s
have simp_rw : s = ⋃ (i : ℕ), s ∩ S i
Tactic: simp_rw [Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
⊢ s = ⋃ (i : ℕ), s ∩ S i
have rw : s = s ∩ ⋃ (i : ℕ), S i
Tactic: rw [← Set.inter_iUnion, iUnion_spanningSets (μ.trim hm), Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
rw : s = s ∩ ⋃ (i : ℕ), S i
⊢ s = ⋃ (i : ℕ), s ∩ S i
have rw₁ : s = s ∩ Set.univ
Tactic: rw [← Set.inter_iUnion, iUnion_spanningSets (μ.trim hm), Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
rw : s = s ∩ ⋃ (i : ℕ), S i
rw₁ : s = s ∩ Set.univ
⊢ s = ⋃ (i : ℕ), s ∩ S i
have rw₂ : s = s
Tactic: rw [← Set.inter_iUnion, iUnion_spanningSets (μ.trim hm), Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have hs_eq : s = ⋃ (i : ℕ), S i ∩ s
Tactic: have hs_eq : s = ⋃ i, S i ∩ s := by
    simp_rw [Set.inter_comm]
    rw [← Set.inter_iUnion, iUnion_spanningSets (μ.trim hm), Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
⊢ ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine fun i => (measure_mono Set.inter_subset_left).trans_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
i : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hS_finite_trim : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim hm) i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hS_finite_trim := measure_spanningSets_lt_top (μ.trim hm) i
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
i : ℕ
hS_finite_trim : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim hm) i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rwa : ∀ (hS_finite_trim : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [trim_measurableSet_eq hm (hS_meas i)] at hS_finite_trim
Cleared hypotheses: hS_finite_trim
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
Tactic: have h_mono : Monotone fun i => S i ∩ s := by
    intro i j hij x
    simp_rw [Set.mem_inter_iff]
    exact fun h => ⟨monotone_spanningSets (μ.trim hm) hij h.1, h.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have h_eq_forall : Eq.{u_3 + 1} (α := (i : ℕ) → F')
  (fun (i : ℕ) ↦
    ∫ (x : α) in S i ∩ s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
  fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
Tactic: have h_eq_forall :
    (fun i => ∫ x in S i ∩ s, condExpL1CLM F' hm μ f x ∂μ) = fun i => ∫ x in S i ∩ s, f x ∂μ :=
    funext fun i =>
      setIntegral_condExpL1CLM_of_measure_ne_top f (@MeasurableSet.inter α m _ _ (hS_meas i) hs)
        (hS_finite i).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
⊢ Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
have h : Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
  (𝓝 (∫ (x : α) in ⋃ (n : ℕ), S n ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
Tactic: have h :=
      tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
        (L1.integrable_coeFn f).integrableOn