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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
c : E
s : Set α
hs : MeasurableSet s
h :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : ¬c = 0
neg :
  ∀ (hp_pos : p ≠ 0), motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)
⊢ motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)

Tactic:
have hp_pos : p ≠ 0 := (lt_of_lt_of_le zero_lt_one _i.elim).ne'
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
c : E
s : Set α
hs : MeasurableSet s
h :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : ¬c = 0
hp_pos : p ≠ 0
⊢ motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)

Tactic:
indicator c hs (SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs h)

Premises used: Set.indicator, MeasureTheory.SimpleFunc.measure_lt_top_of_memLp_indicator, Set.piecewise, ite
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
c : E
s : Set α
hs : MeasurableSet s
h :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : ¬c = 0
hp_pos : p ≠ 0
⊢ motive (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E)

Tactic:
exact indicator c hs (SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs h)

Premises used: MeasureTheory.SimpleFunc.measure_lt_top_of_memLp_indicator
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
f g : α →ₛ E
hfg :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E))
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ → motive (⇑g : (a : α) → E)
int_fg : MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ

Tactic:
rw [SimpleFunc.coe_add,
        memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable] at int_fg

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 α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
f g : α →ₛ E
hfg :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E))
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ → motive (⇑g : (a : α) → E)
int_fg : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ
⊢ motive (⇑(f + g) : (a : α) → E)

Tactic:
add hfg int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2)

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
f g : α →ₛ E
hfg :
  Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
    (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E))
hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ → motive (⇑g : (a : α) → E)
int_fg : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ ∧ MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ
⊢ motive (⇑(f + g) : (a : α) → E)

Tactic:
exact add hfg int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2)

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
⊢ ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)

Tactic:
have : ∀ f : SimpleFunc α E, MemLp f p μ → motive f := by
    apply SimpleFunc.induction
    · intro c s hs h
      by_cases hc : c = 0
      · subst hc; convert! indicator 0 MeasurableSet.empty (by simp) using 1; ext; simp
      have hp_pos : p ≠ 0 := (lt_of_lt_of_le zero_lt_one _i.elim).ne'
      exact indicator c hs (SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs h)
    · intro f g hfg hf hg int_fg
      rw [SimpleFunc.coe_add,
        memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable] at int_fg
      exact add hfg int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2)
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
this : ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
f : ↥(Lp.simpleFunc E p μ)
⊢ motive (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)

Tactic:
ae (Lp.simpleFunc.toSimpleFunc_eq_toFun f) (Lp.simpleFunc.memLp f)
        (this (Lp.simpleFunc.toSimpleFunc f) (Lp.simpleFunc.memLp f))

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.Lp.simpleFunc.memLp, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
this : ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
f : ↥(Lp.simpleFunc E p μ)
⊢ motive (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)

Tactic:
exact
      ae (Lp.simpleFunc.toSimpleFunc_eq_toFun f) (Lp.simpleFunc.memLp f)
        (this (Lp.simpleFunc.toSimpleFunc f) (Lp.simpleFunc.memLp f))

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.Lp.simpleFunc.memLp, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
this : ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
⊢ ∀ (f : ↥(Lp.simpleFunc E p μ)), motive (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)

Tactic:
have : ∀ f : Lp.simpleFunc E p μ, motive f := by
    intro f
    exact
      ae (Lp.simpleFunc.toSimpleFunc_eq_toFun f) (Lp.simpleFunc.memLp f)
        (this (Lp.simpleFunc.toSimpleFunc f) (Lp.simpleFunc.memLp f))
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
this_1 : ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
this : ∀ (f : ↥(Lp.simpleFunc E p μ)), motive (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)
⊢ ∀ (f : ↥(Lp E p μ)), motive (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
have : ∀ f : Lp E p μ, motive f := fun f =>
    (Lp.simpleFunc.denseRange hp_ne_top).induction_on f closed this
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
this_1 : ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
this_2 : ∀ (f : ↥(Lp.simpleFunc E p μ)), motive (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)
this : ∀ (f : ↥(Lp E p μ)), motive (↑(↑f : α →ₘ[μ] E) : α → E)
⊢ ∀ ⦃f : α → E⦄, MemLp f p μ → motive f

Tactic:
fun f hf => ae hf.coeFn_toLp (Lp.memLp _) (this (hf.toLp f))

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.MemLp.toLp, MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f : ↥(Lp E p μ) | motive (↑(↑f : α →ₘ[μ] E) : α → E)}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
this_1 : ∀ (f : α →ₛ E), MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ → motive (⇑f : (a : α) → E)
this_2 : ∀ (f : ↥(Lp.simpleFunc E p μ)), motive (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E)
this : ∀ (f : ↥(Lp E p μ)), motive (↑(↑f : α →ₘ[μ] E) : α → E)
⊢ ∀ ⦃f : α → E⦄, MemLp f p μ → motive f

Tactic:
exact fun f hf => ae hf.coeFn_toLp (Lp.memLp _) (this (hf.toLp f))

Premises used: MeasureTheory.Lp.memLp
-- 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
inl :
  ∀ (hp_ne_top : Ne (α := ℝ≥0∞) 0 ∞)
    (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) 0 μ ≤ ε ∧ P g)
    (hf : MemLp f 0 μ), ∃ (g : α → E), eLpNorm (f - g) 0 μ ≤ ε ∧ P g
inr : ∀ (hp_pos : p ≠ 0), ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g

Tactic:
rcases eq_or_ne p 0 with (rfl | hp_pos)

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
μ : Measure α
P : (α → E) → Prop
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hp_ne_top : Ne (α := ℝ≥0∞) 0 ∞
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) 0 μ ≤ ε ∧ P g
hf : MemLp f 0 μ
⊢ 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
μ : Measure α
P : (α → E) → Prop
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hp_ne_top : Ne (α := ℝ≥0∞) 0 ∞
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) 0 μ ≤ ε ∧ P g
hf : MemLp f 0 μ
inl :
  ∀ (g : α → E),
    eLpNorm (g - Set.indicator ∅ fun (x : α) ↦ 0) 0 μ ≤ ε → ∀ (Pg : P g), ∃ (g : α → E), eLpNorm (f - g) 0 μ ≤ ε ∧ P g
⊢ ∃ (g : α → E), eLpNorm (f - g) 0 μ ≤ ε ∧ P g

Tactic:
rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top])
        hε with ⟨g, _, 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
μ : Measure α
P : (α → E) → Prop
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hp_ne_top : Ne (α := ℝ≥0∞) 0 ∞
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) 0 μ ≤ ε ∧ P g
hf : MemLp f 0 μ
g : α → E
left : eLpNorm (g - Set.indicator ∅ fun (x : α) ↦ 0) 0 μ ≤ ε
Pg : P g
⊢ eLpNorm (f - g) 0 μ ≤ ε

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hp_ne_top : Ne (α := ℝ≥0∞) 0 ∞
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) 0 μ ≤ ε ∧ P g
hf : MemLp f 0 μ
g : α → E
left : eLpNorm (g - Set.indicator ∅ fun (x : α) ↦ 0) 0 μ ≤ ε
Pg : P g
⊢ ∃ (g : α → E), eLpNorm (f - g) 0 μ ≤ ε ∧ P g

Tactic:
exact ⟨g, by simp, 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
obtain :
  ∀ (η : ℝ≥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 - g) p μ ≤ ε ∧ P g
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g

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

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 : α → 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 μ < ε
rcases :
  ∀ (f' : α →ₛ E) (hf' : eLpNorm (f - (⇑f' : (a : α) → E)) p μ < η)
    (f'_mem : MemLp.{u_1, u_4} (ε := E) (⇑f' : (a : α) → E) p μ), ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g

Tactic:
rcases hf.exists_simpleFunc_eLpNorm_sub_lt hp_ne_top ηpos.ne' with ⟨f', hf', f'_mem⟩

Premises used: MeasureTheory.MemLp.exists_simpleFunc_eLpNorm_sub_lt, LT.lt.ne'
-- 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 μ
rcases :
  ∀ (g : α → E) (hg : eLpNorm ((⇑f' : (a : α) → E) - g) p μ ≤ η) (Pg : P g),
    ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g
⊢ ∃ (g : α → E), eLpNorm (f - g) p μ ≤ ε ∧ P g

Tactic:
rcases H f' η ηpos.ne' f'_mem with ⟨g, hg, Pg⟩

Premises used: LT.lt.ne'