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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
⊢ Function.support f ∩ Function.support g =ᶠ[ae μ] ∅
have suffices : Function.support f ∩ Function.support g = ∅
Tactic: suffices Function.support f ∩ Function.support g = ∅ by rw [this]
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
Tactic: have h_inter_empty : (s_f ∩ s_g : Set α) =ᵐ[μ] (∅ : Set α) := by
    refine (hs_f_eq.inter hs_g_eq).trans ?_
    suffices Function.support f ∩ Function.support g = ∅ by rw [this]
    exact Set.disjoint_iff_inter_eq_empty.mp h_disj
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
⊢ s_f \ s_g =ᶠ[ae μ] s_f
have rw : s_f \ (s_f ∩ s_g) =ᶠ[ae μ] s_f
Tactic: rw [← Set.diff_inter_self_eq_diff, Set.inter_comm]
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
⊢ s_f \ (s_f ∩ s_g) =ᶠ[ae μ] s_f
have refine : s_f \ ∅ =ᶠ[ae μ] s_f
Tactic: refine ((ae_eq_refl s_f).diff h_inter_empty).trans ?_
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
⊢ s_f \ ∅ =ᶠ[ae μ] s_f
have rw : s_f =ᶠ[ae μ] s_f
Tactic: rw [Set.diff_empty]
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
⊢ f =ᶠ[ae μ] f'
have this : s_f \ s_g =ᶠ[ae μ] s_f
Tactic: have : s_f \ s_g =ᵐ[μ] s_f := by
      rw [← Set.diff_inter_self_eq_diff, Set.inter_comm]
      refine ((ae_eq_refl s_f).diff h_inter_empty).trans ?_
      rw [Set.diff_empty]
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
this : s_f \ s_g =ᶠ[ae μ] s_f
⊢ f =ᶠ[ae μ] f'
have refine : s_f.indicator (AEStronglyMeasurable.mk f hfm) =ᶠ[ae μ] f
Tactic: refine ((indicator_ae_eq_of_ae_eq_set this).trans ?_).symm
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
this : s_f \ s_g =ᶠ[ae μ] s_f
⊢ s_f.indicator (AEStronglyMeasurable.mk f hfm) =ᶠ[ae μ] f
have rw : AEStronglyMeasurable.mk f hfm =ᶠ[ae μ] f
Tactic: rw [Set.indicator_support]
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have hff' : f =ᶠ[ae μ] f'
Tactic: have hff' : f =ᵐ[μ] f' := by
    have : s_f \ s_g =ᵐ[μ] s_f := by
      rw [← Set.diff_inter_self_eq_diff, Set.inter_comm]
      refine ((ae_eq_refl s_f).diff h_inter_empty).trans ?_
      rw [Set.diff_empty]
    refine ((indicator_ae_eq_of_ae_eq_set this).trans ?_).symm
    rw [Set.indicator_support]
    exact hfm.ae_eq_mk.symm
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
hff' : f =ᶠ[ae μ] f'
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have hf'_meas : StronglyMeasurable f'
Tactic: have hf'_meas : StronglyMeasurable[m] f' := hfm.stronglyMeasurable_mk.indicator (hs_f.diff hs_g)
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
hff' : f =ᶠ[ae μ] f'
hf'_meas : StronglyMeasurable f'
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have hf'_Lp : MemLp f' p μ
Tactic: have hf'_Lp : MemLp f' p μ := hf.ae_eq hff'
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
hff' : f =ᶠ[ae μ] f'
hf'_meas : StronglyMeasurable f'
hf'_Lp : MemLp f' p μ
g' : (x : α) → F := (s_g \ s_f).indicator (AEStronglyMeasurable.mk g hgm)
⊢ s_g \ s_f =ᶠ[ae μ] s_g
have rw : s_g \ (s_f ∩ s_g) =ᶠ[ae μ] s_g
Tactic: rw [← Set.diff_inter_self_eq_diff]
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
hff' : f =ᶠ[ae μ] f'
hf'_meas : StronglyMeasurable f'
hf'_Lp : MemLp f' p μ
g' : (x : α) → F := (s_g \ s_f).indicator (AEStronglyMeasurable.mk g hgm)
⊢ s_g \ (s_f ∩ s_g) =ᶠ[ae μ] s_g
have refine : s_g \ ∅ =ᶠ[ae μ] s_g
Tactic: refine ((ae_eq_refl s_g).diff h_inter_empty).trans ?_
-- 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 : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᶠ[ae μ] ∅
f' : (x : α) → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
hff' : f =ᶠ[ae μ] f'
hf'_meas : StronglyMeasurable f'
hf'_Lp : MemLp f' p μ
g' : (x : α) → F := (s_g \ s_f).indicator (AEStronglyMeasurable.mk g hgm)
⊢ s_g \ ∅ =ᶠ[ae μ] s_g
have rw : s_g =ᶠ[ae μ] s_g
Tactic: rw [Set.diff_empty]