awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
hf'_Lp : MemLp f' p μ
g' : (x : α) → F := (s_g \ s_f).indicator (AEStronglyMeasurable.mk g hgm)
⊢ g =ᶠ[ae μ] g'
have this : s_g \ s_f =ᶠ[ae μ] s_g
Tactic: have : s_g \ s_f =ᵐ[μ] s_g := by
      rw [← Set.diff_inter_self_eq_diff]
      refine ((ae_eq_refl s_g).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)
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)
this : s_g \ s_f =ᶠ[ae μ] s_g
⊢ g =ᶠ[ae μ] g'
have refine : s_g.indicator (AEStronglyMeasurable.mk g hgm) =ᶠ[ae μ] g
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)
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)
this : s_g \ s_f =ᶠ[ae μ] s_g
⊢ s_g.indicator (AEStronglyMeasurable.mk g hgm) =ᶠ[ae μ] g
have rw : AEStronglyMeasurable.mk g hgm =ᶠ[ae μ] g
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)
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)
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have hgg' : g =ᶠ[ae μ] g'
Tactic: have hgg' : g =ᵐ[μ] g' := by
    have : s_g \ s_f =ᵐ[μ] s_g := by
      rw [← Set.diff_inter_self_eq_diff]
      refine ((ae_eq_refl s_g).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 hgm.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'
hf'_meas : StronglyMeasurable f'
hf'_Lp : MemLp f' p μ
g' : (x : α) → F := (s_g \ s_f).indicator (AEStronglyMeasurable.mk g hgm)
hgg' : g =ᶠ[ae μ] g'
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have hg'_meas : StronglyMeasurable g'
Tactic: have hg'_meas : StronglyMeasurable[m] g' := hgm.stronglyMeasurable_mk.indicator (hs_g.diff hs_f)
-- 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'
hf'_Lp : MemLp f' p μ
g' : (x : α) → F := (s_g \ s_f).indicator (AEStronglyMeasurable.mk g hgm)
hgg' : g =ᶠ[ae μ] g'
hg'_meas : StronglyMeasurable g'
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have hg'_Lp : MemLp g' p μ
Tactic: have hg'_Lp : MemLp g' p μ := hg.ae_eq hgg'
-- 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'
hf'_Lp : MemLp f' p μ
g' : (x : α) → F := (s_g \ s_f).indicator (AEStronglyMeasurable.mk g hgm)
hgg' : g =ᶠ[ae μ] g'
hg'_meas : StronglyMeasurable g'
hg'_Lp : MemLp g' p μ
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have h_disj₁ : Disjoint (Function.support f') (Function.support g')
Tactic: have h_disj : Disjoint (Function.support f') (Function.support g') :=
    haveI : Disjoint (s_f \ s_g) (s_g \ s_f) := disjoint_sdiff_sdiff
    this.mono Set.support_indicator_subset Set.support_indicator_subset
-- 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_1 : 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)
hgg' : g =ᶠ[ae μ] g'
hg'_meas : StronglyMeasurable g'
hg'_Lp : MemLp g' p μ
h_disj : Disjoint (Function.support f') (Function.support g')
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have rw : ∀ (hPf : P (MemLp.toLp f' hf'_Lp)),
  let g' := (s_g \ s_f).indicator (AEStronglyMeasurable.mk g hgm);
  ∀ (hgg' : g =ᶠ[ae μ] g') (hg'_meas : StronglyMeasurable g') (hg'_Lp : MemLp g' p μ)
    (h_disj : Disjoint (Function.support f') (Function.support g')), P (MemLp.toLp f' hf'_Lp + MemLp.toLp g hg)
Tactic: rw [← MemLp.toLp_congr hf'_Lp hf hff'.symm] at hPf ⊢
Cleared hypotheses: hPf, g', hgg', hg'_meas, hg'_Lp, 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_1 : Disjoint (Function.support f) (Function.support g)
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 μ
hPf : P (MemLp.toLp f' hf'_Lp)
g' : (x : α) → F := (s_g \ s_f).indicator (AEStronglyMeasurable.mk g hgm)
hgg' : g =ᶠ[ae μ] g'
hg'_meas : StronglyMeasurable g'
hg'_Lp : MemLp g' p μ
h_disj : Disjoint (Function.support f') (Function.support g')
⊢ P (MemLp.toLp f' hf'_Lp + MemLp.toLp g hg)
have rw : ∀ (hPg : P (MemLp.toLp g' hg'_Lp)) (h_disj : Disjoint (Function.support f') (Function.support g')),
  P (MemLp.toLp f' hf'_Lp + MemLp.toLp g' hg'_Lp)
Tactic: rw [← MemLp.toLp_congr hg'_Lp hg hgg'.symm] at hPg ⊢
Cleared hypotheses: hPg, h_disj
-- 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 : α → F
hf : MemLp f p μ
hfm : AEStronglyMeasurable f μ
f_Lp : ↥(Lp F p μ) := toLp f hf
⊢ P f
have hfm_Lp : AEStronglyMeasurable (↑(↑f_Lp : α →ₘ[μ] F) : α → F) μ
Tactic: have hfm_Lp : AEStronglyMeasurable[m] f_Lp μ := hfm.congr hf.coeFn_toLp.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 : (α → 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) μ
⊢ P f
have refine : P (↑(↑(toLp f hf) : α →ₘ[μ] F) : α → F)
Tactic: refine h_ae hf.coeFn_toLp (Lp.memLp _) ?_
-- 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) μ
⊢ P (↑(↑f_Lp : α →ₘ[μ] F) : α → F)
have refine_1 : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (fun (f : ↥(Lp F p μ)) ↦ P (↑(↑f : α →ₘ[μ] F) : α → F))
    (↑(Lp.simpleFunc.indicatorConst p (s := s) sorry sorry c) : ↥(Lp F p μ))
Tactic: refine Lp.induction_stronglyMeasurable hm hp_ne_top (fun f => P f) ?_ ?_ h_closed f_Lp hfm_Lp
-- 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) μ
refine_1 :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (fun (f : ↥(Lp F p μ)) ↦ P (↑(↑f : α →ₘ[μ] F) : α → F))
      (↑(Lp.simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
⊢ P (↑(↑f_Lp : α →ₘ[μ] F) : α → F)
have refine_2 : ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
  StronglyMeasurable f →
    StronglyMeasurable g →
      Disjoint (Function.support f) (Function.support g) →
        (fun (f : ↥(Lp F p μ)) ↦ P (↑(↑f : α →ₘ[μ] F) : α → F)) (toLp f hf) →
          (fun (f : ↥(Lp F p μ)) ↦ P (↑(↑f : α →ₘ[μ] F) : α → F)) (toLp g hg) →
            (fun (f : ↥(Lp F p μ)) ↦ P (↑(↑f : α →ₘ[μ] F) : α → F)) (toLp f hf + toLp g hg)
Tactic: refine Lp.induction_stronglyMeasurable hm hp_ne_top (fun f => P f) ?_ ?_ h_closed f_Lp hfm_Lp