awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
H :
  ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ε
f' : α →ₛ E
hf' : eLpNorm (f - (⇑f' : (a : α) → E)) p μ < η
f'_mem : MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
g : α → E
hg : eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ η
Pg : P g
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g

Tactic:
⟨g, ?_, Pg⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
H :
  ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ε
f' : α →ₛ E
hf' : eLpNorm (f - (⇑f' : (a : α) → E)) p μ < η
f'_mem : MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
g : α → E
hg : eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ η
Pg : P g
refine : eLpNorm (f - g) p μ ≤ ε
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g

Tactic:
refine ⟨g, ?_, Pg⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
H :
  ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ε
f' : α →ₛ E
hf' : eLpNorm (f - (⇑f' : (a : α) → E)) p μ < η
f'_mem : MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
g : α → E
hg : eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ η
Pg : P g
⊢ eLpNorm (f - (⇑f' : (a : α) → E) + ((⇑f' : (a : α) → E) - g)) p μ ≤ ε

Tactic:
(hη _ _ (hf.aestronglyMeasurable.sub f'.aestronglyMeasurable)
          (f'.aestronglyMeasurable.sub (h2P g Pg)) hf'.le hg).le

Premises used: MeasureTheory.AEStronglyMeasurable.sub, LT.lt.le, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.SimpleFunc.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
H :
  ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ε
f' : α →ₛ E
hf' : eLpNorm (f - (⇑f' : (a : α) → E)) p μ < η
f'_mem : MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
g : α → E
hg : eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ η
Pg : P g
h : f - g = f - (⇑f' : (a : α) → E) + ((⇑f' : (a : α) → E) - g)
⊢ eLpNorm (f - g) p μ ≤ ε

Tactic:
convert!
      (hη _ _ (hf.aestronglyMeasurable.sub f'.aestronglyMeasurable)
          (f'.aestronglyMeasurable.sub (h2P g Pg)) hf'.le hg).le using 2

Premises used: MeasureTheory.AEStronglyMeasurable.sub, LT.lt.le, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.SimpleFunc.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
H :
  ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ε
f' : α →ₛ E
hf' : eLpNorm (f - (⇑f' : (a : α) → E)) p μ < η
f'_mem : MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
g : α → E
hg : eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ η
Pg : P g
⊢ f - g = f - (⇑f' : (a : α) → E) + ((⇑f' : (a : α) → E) - g)

Tactic:
simp only [sub_add_sub_cancel]

Premises used: sub_add_sub_cancel
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
inr :
  ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g

Tactic:
suffices H : ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0), MemLp f' p μ →
      ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g by
    obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p hε
    rcases hf.exists_simpleFunc_eLpNorm_sub_lt hp_ne_top ηpos.ne' with ⟨f', hf', f'_mem⟩
    rcases H f' η ηpos.ne' f'_mem with ⟨g, hg, Pg⟩
    refine ⟨g, ?_, Pg⟩
    convert!
      (hη _ _ (hf.aestronglyMeasurable.sub f'.aestronglyMeasurable)
          (f'.aestronglyMeasurable.sub (h2P g Pg)) hf'.le hg).le using 2
    simp only [sub_add_sub_cancel]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
inr :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
        p μ →
      ∃ (g : α → E),
        eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤
            δ ∧
          P g
inr₁ :
  ∀ ⦃f g : α →ₛ E⦄,
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      (∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
          MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ →
            ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g) →
        (∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
            MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ →
              ∃ (g_1 : α → E), eLpNorm ((⇑g : (a : α) → E) - g_1) p μ ≤ δ ∧ P g_1) →
          ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
            MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ →
              ∃ (g_1 : α → E), eLpNorm ((⇑(f + g) : (a : α) → E) - g_1) p μ ≤ δ ∧ P g_1
⊢ ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ δ ∧ P g

Tactic:
apply SimpleFunc.induction
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
c : E
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
inr :
  ∀
    (Hs :
      MemLp.{u_1, u_4} (ε := E)
        (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p μ),
    ∃ (g : α → E),
      eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
        P g
inr₁ :
  ∀ (hc : c ≠ 0),
    ∃ (g : α → E),
      eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
        P g
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [measure_empty, zero_lt_top]

Premises used: ENNReal.zero_lt_top, MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
inr :
  ∀ (g : α → E) (hg : eLpNorm (g - Set.indicator ∅ fun (x : α) ↦ 0) p μ ≤ ε) (Pg : P g),
    ∃ (g : α → E),
      eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
        P g
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g

Tactic:
rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top])
          εpos with ⟨g, hg, Pg⟩

Premises used: MeasurableSet.empty, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
g : α → E
hg : eLpNorm (g - Set.indicator ∅ fun (x : α) ↦ 0) p μ ≤ ε
Pg : P g
⊢ eLpNorm ((Set.indicator ∅ fun (x : α) ↦ 0) - g) p μ ≤ ε

Tactic:
rw [← eLpNorm_neg, neg_sub] at hg

Premises used: neg_sub, MeasureTheory.eLpNorm_neg
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
g : α → E
hg : eLpNorm (g - Set.indicator ∅ fun (x : α) ↦ 0) p μ ≤ ε
Pg : P g
hg₁ : eLpNorm ((Set.indicator ∅ fun (x : α) ↦ 0) - g) p μ ≤ ε
⊢ P g

Tactic:
rw [← eLpNorm_neg, neg_sub] at hg

Premises used: neg_sub, MeasureTheory.eLpNorm_neg
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
g : α → E
hg : eLpNorm ((Set.indicator ∅ fun (x : α) ↦ 0) - g) p μ ≤ ε
Pg : P g
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g

Tactic:
⟨g, ?_, Pg⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
g : α → E
hg : eLpNorm ((Set.indicator ∅ fun (x : α) ↦ 0) - g) p μ ≤ ε
Pg : P g
inr : eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g

Tactic:
refine ⟨g, ?_, Pg⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
g : α → E
hg : eLpNorm ((Set.indicator ∅ fun (x : α) ↦ 0) - g) p μ ≤ ε
Pg : P g
⊢ eLpNorm ((Set.indicator ∅ fun (x : α) ↦ 0) - g) p μ ≤ ε

Tactic:
hg
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
g : α → E
hg : eLpNorm ((Set.indicator ∅ fun (x : α) ↦ 0) - g) p μ ≤ ε
Pg : P g
h :
  Eq (α := (a : α) → E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
    (Set.indicator ∅ fun (x : α) ↦ 0)
⊢ eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε

Tactic:
convert! hg
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
g : α → E
hg : eLpNorm ((Set.indicator ∅ fun (x : α) ↦ 0) - g) p μ ≤ ε
Pg : P g
h :
  ∀ (x : α),
    Eq.{u_4 + 1} (α := E)
      ((SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0) : (a : α) → E) x : E)
      (Set.indicator ∅ (fun (x : α) ↦ 0) x : E)
⊢ Eq (α := (a : α) → E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
    (Set.indicator ∅ fun (x : α) ↦ 0)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
g : α → E
hg : eLpNorm ((Set.indicator ∅ fun (x : α) ↦ 0) - g) p μ ≤ ε
Pg : P g
x : α
⊢ Eq.{u_4 + 1} (α := E) ((SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0) : (a : α) → E) x : E)
    (Set.indicator ∅ (fun (x : α) ↦ 0) x : E)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ (g : α → E), eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε : ε_1 ≠ 0
hp_pos : p ≠ 0
c : E
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : c ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have : μ s < ∞ := SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs Hs