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 μ
ε_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
this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inr :
  ∀ (g : α → E) (hg : eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε) (Pg : P g),
    ∃ (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 h0P c hs this εpos with ⟨g, hg, 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
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
this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → E
hg : eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε
Pg : P g
⊢ eLpNorm ((s.indicator fun (x : α) ↦ c) - 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
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
this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → E
hg : eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε
Pg : P g
hg₁ : eLpNorm ((s.indicator fun (x : α) ↦ c) - 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
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
this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → E
hg : eLpNorm ((s.indicator fun (x : α) ↦ c) - g) p μ ≤ ε
Pg : P g
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g

Tactic:
⟨g, hg, 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
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
this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → E
hg : eLpNorm ((s.indicator fun (x : α) ↦ c) - g) p μ ≤ ε
Pg : P g
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g

Tactic:
exact ⟨g, hg, 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_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥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
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑(f + f') : (a : α) → E) p μ
inr :
  ∀ (η : ℝ≥0∞) (ηpos : 0 < η)
    (hη :
      ∀ (f g : α → E),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ),
    ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g

Tactic:
obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p δpos

Premises used: MeasureTheory.exists_Lp_half
-- 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_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥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
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑(f + f') : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
inr :
  ∀ (int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ)
    (η : ℝ≥0∞) (ηpos : 0 < η)
    (hη :
      ∀ (f g : α → E),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ),
    ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g

Tactic:
rw [SimpleFunc.coe_add,
      memLp_add_of_disjoint hff' f.stronglyMeasurable f'.stronglyMeasurable] at int_ff'

Premises used: MeasureTheory.SimpleFunc.coe_add, MeasureTheory.memLp_add_of_disjoint, MeasureTheory.SimpleFunc.stronglyMeasurable
-- 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_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥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
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
inr :
  ∀ (g : α → E) (hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η) (Pg : P g),
    ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g

Tactic:
rcases hf η ηpos.ne' int_ff'.1 with ⟨g, hg, Pg⟩

Premises used: LT.lt.ne', And.left
-- 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_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥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
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
inr :
  ∀ (g' : α → E) (hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η) (Pg' : P g'),
    ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g

Tactic:
rcases hf' η ηpos.ne' int_ff'.2 with ⟨g', hg', Pg'⟩

Premises used: LT.lt.ne', And.right
-- 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_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥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
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
g' : α → E
hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η
Pg' : P g'
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g

Tactic:
⟨g + g', ?_, h1P g g' Pg Pg'⟩

Premises used: HAdd.hAdd, 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_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥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
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
g' : α → E
hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η
Pg' : P g'
inr : eLpNorm ((⇑(f + f') : (a : α) → E) - (g + g')) p μ ≤ δ
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g

Tactic:
refine ⟨g + g', ?_, h1P g g' Pg 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_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥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
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
g' : α → E
hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η
Pg' : P g'
⊢ eLpNorm ((⇑f : (a : α) → E) - g + ((⇑f' : (a : α) → E) - g')) p μ ≤ δ

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

Premises used: MeasureTheory.AEStronglyMeasurable.sub, LT.lt.le, 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_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥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
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
g' : α → E
hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η
Pg' : P g'
h : (⇑(f + f') : (a : α) → E) - (g + g') = (⇑f : (a : α) → E) - g + ((⇑f' : (a : α) → E) - g')
⊢ eLpNorm ((⇑(f + f') : (a : α) → E) - (g + g')) p μ ≤ δ

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

Premises used: MeasureTheory.AEStronglyMeasurable.sub, LT.lt.le, 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_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥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
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
g' : α → E
hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η
Pg' : P g'
h :
  HAdd.hAdd (α := (a : α) → E) (⇑f : (a : α) → E) (⇑f' : (a : α) → E) - (g + g') =
    (⇑f : (a : α) → E) - g + ((⇑f' : (a : α) → E) - g')
⊢ (⇑(f + f') : (a : α) → E) - (g + g') = (⇑f : (a : α) → E) - g + ((⇑f' : (a : α) → E) - g')

Tactic:
rw [SimpleFunc.coe_add]

Premises used: MeasureTheory.SimpleFunc.coe_add
-- 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_1 : α → E
hf_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑f' : (a : α) → E))
hf :
  ∀ (δ : ℝ≥0∞) (hδ : δ ≠ 0),
    MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → ∃ (g : α → E), eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ δ ∧ P g
hf' :
  ∀ (δ : ℝ≥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
int_ff' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm ((⇑f : (a : α) → E) - g) p μ ≤ η
Pg : P g
g' : α → E
hg' : eLpNorm ((⇑f' : (a : α) → E) - g') p μ ≤ η
Pg' : P g'
⊢ HAdd.hAdd (α := (a : α) → E) (⇑f : (a : α) → E) (⇑f' : (a : α) → E) - (g + g') =
    (⇑f : (a : α) → E) - g + ((⇑f' : (a : α) → E) - g')

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
f : α →ₛ E
hf : Integrable.{u_4, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ (↑(f.toLp ⋯) : ↥(Lp E 1 μ)) = Integrable.toL1 (⇑f : (a : α) → E) hf

Tactic:
rfl

Premises used: MeasureTheory.MemLp.toLp, MeasureTheory.Integrable.toL1, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
f : ↥(Lp.simpleFunc E 1 μ)
rw : MemLp.{u_1, u_4} (ε := E) (⇑(Lp.simpleFunc.toSimpleFunc f) : (a : α) → E) 1 μ
⊢ Integrable.{u_4, u_1} (ε := E) (⇑(Lp.simpleFunc.toSimpleFunc f) : (a : α) → E) μ

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable