awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind :
  ∀ (c : F) ⦃s : Set α⦄,
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → P (s.indicator fun (x : α) ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed :
  IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f : α → F
hf : MemLp f p μ
hfm : AEStronglyMeasurable f μ
f_Lp : ↥(Lp F p μ) := toLp f hf
hfm_Lp : AEStronglyMeasurable (↑(↑f_Lp : α →ₘ[μ] F) : α → F) μ
c : F
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ P (↑(↑(↑(Lp.simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)
have refine_1 : P (↑(↑(indicatorConstLp (s := s) p sorry sorry c) : α →ₘ[μ] F) : α → F)
Tactic: rw [Lp.simpleFunc.coe_indicatorConst]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind :
  ∀ (c : F) ⦃s : Set α⦄,
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → P (s.indicator fun (x : α) ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed :
  IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f : α → F
hf : MemLp f p μ
hfm : AEStronglyMeasurable f μ
f_Lp : ↥(Lp F p μ) := toLp f hf
hfm_Lp : AEStronglyMeasurable (↑(↑f_Lp : α →ₘ[μ] F) : α → F) μ
c : F
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ P (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
have refine_1 : MemLp.{u_1, u_2} (ε := F) (s.indicator fun (x : α) ↦ c) p μ
Tactic: refine h_ae indicatorConstLp_coeFn.symm ?_ (h_ind c hs hμs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind :
  ∀ (c : F) ⦃s : Set α⦄,
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → P (s.indicator fun (x : α) ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed :
  IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f_1 : α → F
hf : MemLp f_1 p μ
hfm_1 : AEStronglyMeasurable f_1 μ
f_Lp : ↥(Lp F p μ) := toLp f_1 hf
hfm_Lp : AEStronglyMeasurable (↑(↑f_Lp : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (↑(↑(toLp f hf_mem) : α →ₘ[μ] F) : α → F)
hgP : P (↑(↑(toLp g hg_mem) : α →ₘ[μ] F) : α → F)
⊢ P (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → F)
have refine_2 : ∀ (hfP' : P f), P (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → F)
Tactic: have hfP' : P f := h_ae hf_mem.coeFn_toLp (Lp.memLp _) hfP
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (hypothesis)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind :
  ∀ (c : F) ⦃s : Set α⦄,
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → P (s.indicator fun (x : α) ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed :
  IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f_1 : α → F
hf : MemLp f_1 p μ
hfm_1 : AEStronglyMeasurable f_1 μ
f_Lp : ↥(Lp F p μ) := toLp f_1 hf
hfm_Lp : AEStronglyMeasurable (↑(↑f_Lp : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (↑(↑(toLp f hf_mem) : α →ₘ[μ] F) : α → F)
hgP : P (↑(↑(toLp g hg_mem) : α →ₘ[μ] F) : α → F)
hfP' : P f
⊢ P (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → F)
have hgP' : P g
Tactic: have hgP' : P g := h_ae hg_mem.coeFn_toLp (Lp.memLp _) hgP
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (hypothesis)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind :
  ∀ (c : F) ⦃s : Set α⦄,
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → P (s.indicator fun (x : α) ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed :
  IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f_1 : α → F
hf : MemLp f_1 p μ
hfm_1 : AEStronglyMeasurable f_1 μ
f_Lp : ↥(Lp F p μ) := toLp f_1 hf
hfm_Lp : AEStronglyMeasurable (↑(↑f_Lp : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (↑(↑(toLp f hf_mem) : α →ₘ[μ] F) : α → F)
hgP : P (↑(↑(toLp g hg_mem) : α →ₘ[μ] F) : α → F)
hfP' : P f
hgP' : P g
⊢ P (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → F)
have h_add₁ : P (f + g)
Tactic: specialize h_add h_disj hf_mem hg_mem hfm hgm hfP' hgP'
Cleared hypotheses: h_add
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind :
  ∀ (c : F) ⦃s : Set α⦄,
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → P (s.indicator fun (x : α) ↦ c)
h_closed :
  IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f_1 : α → F
hf : MemLp f_1 p μ
hfm_1 : AEStronglyMeasurable f_1 μ
f_Lp : ↥(Lp F p μ) := toLp f_1 hf
hfm_Lp : AEStronglyMeasurable (↑(↑f_Lp : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (↑(↑(toLp f hf_mem) : α →ₘ[μ] F) : α → F)
hgP : P (↑(↑(toLp g hg_mem) : α →ₘ[μ] F) : α → F)
hfP' : P f
hgP' : P g
h_add : P (f + g)
⊢ P (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → F)
have refine_2 : f + g =ᶠ[ae μ] (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → F)
Tactic: refine h_ae ?_ (hf_mem.add hg_mem) h_add
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm_not : ¬m ≤ m₀
⊢ μ[f | m] = 0
have rw : Eq (α := α → E)
  (if hm : m ≤ m₀ then
    if h : SigmaFinite (μ.trim hm) ∧ Integrable f μ then
      if StronglyMeasurable f then f
      else
        have this := sorry;
        AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry
    else 0
  else 0)
  0
Tactic: rw [condExp, dif_neg hm_not]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm_not : ¬m ≤ m₀
rw :
  Eq (α := α → E)
    (if hm : m ≤ m₀ then
      if h : SigmaFinite (μ.trim hm) ∧ Integrable f μ then
        if StronglyMeasurable f then f
        else
          have this := ⋯;
          AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
      else 0
    else 0)
    0
⊢ μ[f | m] = 0
have rw₁ : Eq (α := α → E) 0 0
Tactic: rw [condExp, dif_neg hm_not]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm_not : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] = 0
have hnc : ¬(SigmaFinite (μ.trim hm) ∧ Integrable f μ)
Tactic: rw [condExp, dif_pos hm, dif_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm_not : ¬SigmaFinite (μ.trim hm)
⊢ ¬(SigmaFinite (μ.trim hm) ∧ Integrable f μ)
have hnc : ∀ (_ : SigmaFinite (μ.trim hm)), ¬Integrable f μ
Tactic: push Not
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f | m] =
    if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0
have rw : (if h : SigmaFinite (μ.trim hm) ∧ Integrable f μ then
    if StronglyMeasurable f then f
    else
      have this := sorry;
      AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry
  else 0) =
  if Integrable f μ then
    if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry
  else 0
Tactic: rw [condExp, dif_pos hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ μ[f | m] = f
have rw : (if Integrable f μ then
    if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry
  else 0) =
  f
Tactic: rw [condExp_of_sigmaFinite hm, if_pos hfi, if_pos hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : StronglyMeasurable f
hfi : Integrable f μ
rw :
  (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0) =
    f
⊢ μ[f | m] = f
have rw₁ : (if StronglyMeasurable f then f
  else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry) =
  f
Tactic: rw [condExp_of_sigmaFinite hm, if_pos hfi, if_pos hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : StronglyMeasurable f
hfi : Integrable f μ
rw :
  (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0) =
    f
rw₁ :
  (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =
    f
⊢ μ[f | m] = f
have rw₂ : f = f
Tactic: rw [condExp_of_sigmaFinite hm, if_pos hfi, if_pos hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
⊢ μ[f | m] =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
have rw : (if Integrable f μ then
    if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry
  else 0) =ᶠ[ae μ]
  (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
Tactic: rw [condExp_of_sigmaFinite hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
⊢ (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
have pos : ∀ (hfi : Integrable f μ),
  (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry
    else 0) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
pos :
  ∀ (hfi : Integrable f μ),
    (if Integrable f μ then
        if StronglyMeasurable f then f
        else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
      else 0) =ᶠ[ae μ]
      (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
⊢ (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
have neg : ∀ (hfi : ¬Integrable f μ),
  (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry
    else 0) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
⊢ (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
have pos : (if StronglyMeasurable f then f
  else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry) =ᶠ[ae μ]
  (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
Tactic: rw [if_pos hfi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
⊢ (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
have pos : ∀ (hfm : StronglyMeasurable f),
  (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
Tactic: by_cases hfm : StronglyMeasurable[m] f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
pos :
  ∀ (hfm : StronglyMeasurable f),
    (if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[ae μ]
      (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
⊢ (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
have neg : ∀ (hfm : ¬StronglyMeasurable f),
  (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
Tactic: by_cases hfm : StronglyMeasurable[m] f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
have pos : f =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
Tactic: rw [if_pos hfm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
⊢ (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
have neg : AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry =ᶠ[ae μ]
  (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
Tactic: rw [if_neg hfm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : ¬Integrable f μ
⊢ (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
have neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 (↑(↑0 : α →ₘ[μ] E) : α → E)
Tactic: rw [if_neg hfi, condExpL1_undef hfi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
hf : Integrable f μ
⊢ μ[f | m] =ᶠ[ae μ]
    (↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E)
have refine : ∀ (x : α),
  (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) x =
    (↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E) x
Tactic: refine (condExp_ae_eq_condExpL1 hm f).trans (Eventually.of_forall fun x => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
hf : Integrable f μ
x : α
⊢ (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) x =
    (↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E) x
have rw : Eq.{u_3 + 1} (α := E)
  ((↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E) x)
  ((↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E) x)
Tactic: rw [condExpL1_eq hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
⊢ μ[f | m] = 0
have pos : ∀ (hm : m ≤ m₀), μ[f | m] = 0
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
pos : ∀ (hm : m ≤ m₀), μ[f | m] = 0
⊢ μ[f | m] = 0
have neg : ∀ (hm : ¬m ≤ m₀), μ[f | m] = 0
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : ¬m ≤ m₀
⊢ μ[f | m] = 0
have neg : Eq (α := α → E) 0 0
Tactic: rw [condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
⊢ μ[f | m] = 0
have pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] = 0
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] = 0
⊢ μ[f | m] = 0
have neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f | m] = 0
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)