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 : ↥(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 μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable 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' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f_1 hf_1
g_1 : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g_1
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (MemLp.toLp f ⋯)
hgP : P (MemLp.toLp g ⋯)
h_eq :
  ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp f hf)) :
        ↥(Lp F p μ)) =
      MemLp.toLp f ⋯
⊢ P (MemLp.toLp f ⋯ + MemLp.toLp g ⋯)

Tactic:
h_add (memLp_of_memLp_trim hm hf) (memLp_of_memLp_trim hm hg)
      (hf.aestronglyMeasurable.of_trim hm) (hg.aestronglyMeasurable.of_trim hm) h_disj hfP hgP

Premises used: Set.Mem, MeasureTheory.AEStronglyMeasurable.of_trim, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.memLp_of_memLp_trim
-- 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 : ↥(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 μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable 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' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f_1 hf_1
g_1 : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g_1
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (MemLp.toLp f ⋯)
hgP : P (MemLp.toLp g ⋯)
h_eq :
  ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp f hf)) :
        ↥(Lp F p μ)) =
      MemLp.toLp f ⋯
⊢ P (MemLp.toLp f ⋯ + MemLp.toLp g ⋯)

Tactic:
exact h_add (memLp_of_memLp_trim hm hf) (memLp_of_memLp_trim hm hg)
      (hf.aestronglyMeasurable.of_trim hm) (hg.aestronglyMeasurable.of_trim hm) h_disj hfP hgP

Premises used: MeasureTheory.AEStronglyMeasurable.of_trim, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.memLp_of_memLp_trim
-- 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 : ↥(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 μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable 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 : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
refine_3 :
  IsClosed (X := ↥(Lp F p (μ.trim hm)))
    (Set.preimage (β := ↥(lpMeas F ℝ m p μ))
      (⇑(LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm)) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
      {g : ↥(lpMeas F ℝ m p μ) | P (↑g : ↥(Lp F p μ))})
⊢ IsClosed (X := ↥(Lp F p (μ.trim hm)))
    {f : ↥(Lp F p (μ.trim hm)) |
      (fun (g : ↥(Lp F p (μ.trim hm))) ↦
          P
            (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                    (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                  g) :
              ↥(Lp F p μ)))
        f}

Tactic:
change IsClosed ((lpMeasToLpTrimLie F ℝ p μ hm).symm ⁻¹' {g : lpMeas F ℝ m p μ | P ↑g})

Premises used: Real, LinearIsometryEquiv.symm, MeasureTheory.lpMeasToLpTrimLie, setOf, IsClosed, Set.preimage, Subtype.val, DFunLike.coe
-- 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 : ↥(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 μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable 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 : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
⊢ IsClosed (X := ↥(Lp F p (μ.trim hm)))
    (Set.preimage (β := ↥(lpMeas F ℝ m p μ))
      (⇑(LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm)) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
      {g : ↥(lpMeas F ℝ m p μ) | P (↑g : ↥(Lp F p μ))})

Tactic:
IsClosed.preimage (LinearIsometryEquiv.continuous _) h_closed

Premises used: IsClosed.preimage, LinearIsometryEquiv.continuous
-- 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 : ↥(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 μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable 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 : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
⊢ IsClosed (X := ↥(Lp F p (μ.trim hm)))
    (Set.preimage (β := ↥(lpMeas F ℝ m p μ))
      (⇑(LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm)) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
      {g : ↥(lpMeas F ℝ m p μ) | P (↑g : ↥(Lp F p μ))})

Tactic:
exact IsClosed.preimage (LinearIsometryEquiv.continuous _) h_closed

Premises used: IsClosed.preimage, LinearIsometryEquiv.continuous
-- 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 : ↥(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 : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
suffices :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable 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)
⊢ P f

Tactic:
suffices h_add_ae :
    ∀ ⦃f g⦄, ∀ hf : MemLp f p μ, ∀ hg : MemLp g p μ, AEStronglyMeasurable[m] f μ →
      AEStronglyMeasurable[m] g μ → Disjoint (Function.support f) (Function.support g) →
        P (hf.toLp f) → P (hg.toLp g) → P (hf.toLp f + hg.toLp g) from
    Lp.induction_stronglyMeasurable_aux hm hp_ne_top _ h_ind h_add_ae h_closed f hf
-- 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 : ↥(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)
let : P (MemLp.toLp f hf + MemLp.toLp g hg)
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)

Tactic:
let s_f : Set α := Function.support (hfm.mk f)
-- 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 : ↥(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)
⊢ MeasurableSet s_f

Tactic:
have hs_f : MeasurableSet[m] s_f := hfm.stronglyMeasurable_mk.measurableSet_support
-- 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 : ↥(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
⊢ s_f =ᶠ[ae μ] Function.support f

Tactic:
have hs_f_eq : s_f =ᵐ[μ] Function.support f := hfm.ae_eq_mk.symm.support
-- 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 : ↥(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)
⊢ MeasurableSet s_g

Tactic:
have hs_g : MeasurableSet[m] s_g := hgm.stronglyMeasurable_mk.measurableSet_support
-- 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 : ↥(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
⊢ s_g =ᶠ[ae μ] Function.support g

Tactic:
have hs_g_eq : s_g =ᵐ[μ] Function.support g := hgm.ae_eq_mk.symm.support
-- 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 : ↥(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
⊢ s_f ∩ s_g =ᶠ[ae μ] ∅

Tactic:
(hs_f_eq.inter hs_g_eq).trans ?_

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.inter
-- 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 : ↥(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
refine : Function.support f ∩ Function.support g =ᶠ[ae μ] ∅
⊢ s_f ∩ s_g =ᶠ[ae μ] ∅

Tactic:
refine (hs_f_eq.inter hs_g_eq).trans ?_

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.inter
-- 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 : ↥(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
this : Function.support f ∩ Function.support g = ∅
rw rw₁ : (ae μ).EventuallyEq (β := Prop) ∅ ∅
⊢ Function.support f ∩ Function.support g =ᶠ[ae μ] ∅

Tactic:
rw [this]