awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
have refine : eLpNorm (f - g) p μ ≤ ε
Tactic: refine ⟨g, ?_, Pg⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 - g) p μ ≤ ε
have h : f - g = f - (⇑f' : (a : α) → E) + ((⇑f' : (a : α) → E) - g)
Tactic: convert!
      (hη _ _ (hf.aestronglyMeasurable.sub f'.aestronglyMeasurable)
          (f'.aestronglyMeasurable.sub (h2P g Pg)) hf'.le hg).le using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
have 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
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
⊢ ∀ (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
have 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
Tactic: apply SimpleFunc.induction
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
⊢ ∀ (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
have 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
Tactic: apply SimpleFunc.induction
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
    μ
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g
have 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
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
Cleared hypotheses: c, Hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g
have inr₁ : ∀ (hc : c ≠ 0),
  ∃ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g
have 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
Tactic: rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top])
          εpos with ⟨g, hg, Pg⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g
have hg₁ : eLpNorm ((Set.indicator ∅ fun (x : α) ↦ 0) - g) p μ ≤ ε
Tactic: rw [← eLpNorm_neg, neg_sub] at hg
Cleared hypotheses: hg, Pg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
have inr : eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε
Tactic: refine ⟨g, ?_, Pg⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε
have h : Eq (α := (a : α) → E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
  (Set.indicator ∅ fun (x : α) ↦ 0)
Tactic: convert! hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
⊢ Eq (α := (a : α) → E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) : (a : α) → E)
    (Set.indicator ∅ fun (x : α) ↦ 0)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g
have 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
Tactic: rcases h0P c hs this εpos with ⟨g, hg, Pg⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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
⊢ ∃ (g : α → E),
    eLpNorm ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) - g) p μ ≤ ε ∧
      P g
have hg₁ : eLpNorm ((s.indicator fun (x : α) ↦ c) - g) p μ ≤ ε
Tactic: rw [← eLpNorm_neg, neg_sub] at hg
Cleared hypotheses: hg, Pg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 μ
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
have 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
Tactic: obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p δpos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 μ < δ
⊢ ∃ (g : α → E), eLpNorm ((⇑(f + f') : (a : α) → E) - g) p μ ≤ δ ∧ P g
have 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
Tactic: rw [SimpleFunc.coe_add,
      memLp_add_of_disjoint hff' f.stronglyMeasurable f'.stronglyMeasurable] at int_ff'
Cleared hypotheses: int_ff', η, ηpos, hη