awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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∞)
refine_1 : P (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
⊢ P (↑(↑(↑(Lp.simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)

Tactic:
rw [Lp.simpleFunc.coe_indicatorConst]

Premises used: MeasureTheory.Lp.simpleFunc.coe_indicatorConst
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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)

Tactic:
h_ae indicatorConstLp_coeFn.symm ?_ (h_ind c hs hμs)

Premises used: MeasureTheory.indicatorConstLp_coeFn, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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∞)
refine_1 : MemLp.{u_1, u_2} (ε := F) (s.indicator fun (x : α) ↦ c) p μ
⊢ P (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)

Tactic:
refine h_ae indicatorConstLp_coeFn.symm ?_ (h_ind c hs hμs)

Premises used: MeasureTheory.indicatorConstLp_coeFn, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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∞)
⊢ MemLp.{u_1, u_2} (ε := F) (s.indicator fun (x : α) ↦ c) p μ

Tactic:
memLp_indicator_const p (hm s hs) c (Or.inr hμs.ne)

Premises used: MeasureTheory.memLp_indicator_const, Or.inr, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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∞)
⊢ MemLp.{u_1, u_2} (ε := F) (s.indicator fun (x : α) ↦ c) p μ

Tactic:
exact memLp_indicator_const p (hm s hs) c (Or.inr hμs.ne)

Premises used: MeasureTheory.memLp_indicator_const, Or.inr, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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)
refine_2 : ∀ (hfP' : P f), P (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → 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
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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 g

Tactic:
have hgP' : P g := h_ae hg_mem.coeFn_toLp (Lp.memLp _) hgP
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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 (f + g)

Tactic:
specialize h_add h_disj hf_mem hg_mem hfm hgm hfP' hgP'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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)

Tactic:
h_ae ?_ (hf_mem.add hg_mem) h_add

Premises used: MeasureTheory.MemLp.add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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)
refine_2 : f + g =ᶠ[ae μ] (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → F)
⊢ P (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → F)

Tactic:
refine h_ae ?_ (hf_mem.add hg_mem) h_add

Premises used: MeasureTheory.MemLp.add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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)
⊢ f + g =ᶠ[ae μ] (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → F)

Tactic:
(hf_mem.coeFn_toLp.symm.add hg_mem.coeFn_toLp.symm).trans (Lp.coeFn_add _ _).symm

Premises used: MeasureTheory.Lp.coeFn_add, Filter.EventuallyEq.trans, MeasureTheory.MemLp.coeFn_toLp, Filter.EventuallyEq.add, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
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)
⊢ f + g =ᶠ[ae μ] (↑(↑(toLp f hf_mem + toLp g hg_mem) : α →ₘ[μ] F) : α → F)

Tactic:
exact (hf_mem.coeFn_toLp.symm.add hg_mem.coeFn_toLp.symm).trans (Lp.coeFn_add _ _).symm

Premises used: MeasureTheory.Lp.coeFn_add, Filter.EventuallyEq.trans, MeasureTheory.MemLp.coeFn_toLp, Filter.EventuallyEq.add, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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
rw₁ rw₂ : Eq (α := α → E) 0 0
⊢ μ[f | m] = 0

Tactic:
rw [condExp, dif_neg hm_not]

Premises used: MeasureTheory.condExp, dif_neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)
hnc : ¬(SigmaFinite (μ.trim hm) ∧ Integrable f μ)
⊢ μ[f | m] = 0

Tactic:
rw [condExp, dif_pos hm, dif_neg]

Premises used: dif_pos, MeasureTheory.condExp, dif_neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)
hnc : ∀ (_ : SigmaFinite (μ.trim hm)), ¬Integrable f μ
⊢ ¬(SigmaFinite (μ.trim hm) ∧ Integrable f μ)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 μ

Tactic:
fun h => absurd h hμm_not

Premises used: absurd
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 μ

Tactic:
exact fun h => absurd h hμm_not

Premises used: absurd
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)
rw :
  (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) =
    if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0
⊢ μ[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

Tactic:
rw [condExp, dif_pos hm]

Premises used: dif_pos, MeasureTheory.condExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)
⊢ (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) =
    if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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
rw₂ rw₃ : f = f
⊢ μ[f | m] = f

Tactic:
rw [condExp_of_sigmaFinite hm, if_pos hfi, if_pos hf]

Premises used: if_pos, MeasureTheory.condExp_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
c : E
inst_2 : IsFiniteMeasure μ
⊢ Eq (α := α → E) μ[fun (x : α) ↦ c | m] fun (x : α) ↦ c

Tactic:
condExp_of_stronglyMeasurable hm stronglyMeasurable_const (integrable_const c)

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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
rw :
  (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)
⊢ μ[f | m] =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)

Tactic:
rw [condExp_of_sigmaFinite hm]

Premises used: MeasureTheory.condExp_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)
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) ⋯
      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)

Tactic:
by_cases hfi : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 :
  (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[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)

Tactic:
rw [if_pos hfi]

Premises used: if_pos