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_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
pos : ∀ (hc : c = 0), P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)
neg : ∀ (hc : ¬c = 0), P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)
⊢ P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  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∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

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_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : c = 0
h :
  (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf =
    simpleFunc.indicatorConst p (s := ∅) ⋯ ⋯ 0
⊢ P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)

Tactic:
convert! indicatorConst 0 MeasurableSet.empty (by simp) using 1

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_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : c = 0
h :
  (↑((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf) : ↥(Lp E p μ)) =
    (↑(simpleFunc.indicatorConst p (s := ∅) ⋯ ⋯ 0) : ↥(Lp E p μ))
⊢ (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf =
    simpleFunc.indicatorConst p (s := ∅) ⋯ ⋯ 0

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : c = 0
⊢ (↑((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf) : ↥(Lp E p μ)) =
    (↑(simpleFunc.indicatorConst p (s := ∅) ⋯ ⋯ 0) : ↥(Lp E p μ))

Tactic:
simp [hc]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : ¬c = 0
⊢ P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)

Tactic:
indicatorConst c hs
      (SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs hf)

Premises used: MeasureTheory.Lp.simpleFunc.indicatorConst, 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 α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf :
  MemLp.{u_1, u_4} (ε := E) (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) : (a : α) → E) p
    μ
hc : ¬c = 0
⊢ P ((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf)

Tactic:
exact indicatorConst c hs
      (SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs hf)

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 α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
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 : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
hg : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ), P (g.toLp hf)
hfg' : 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:
(memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable).mp hfg'

Premises used: MeasureTheory.memLp_add_of_disjoint, Iff.mp, 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_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
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 : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
hg : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ), P (g.toLp hf)
hfg' : MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ
⊢ MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ

Tactic:
obtain ⟨hf', hg'⟩ : MemLp f p μ ∧ MemLp g p μ :=
      (memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable).mp hfg'

Premises used: MeasureTheory.MemLp, MeasureTheory.memLp_add_of_disjoint, Iff.mp, MeasureTheory.SimpleFunc.stronglyMeasurable, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
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 : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
hg : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ), P (g.toLp hf)
hfg' : MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ
hf' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
⊢ MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ

Tactic:
obtain ⟨hf', hg'⟩ : MemLp f p μ ∧ MemLp g p μ :=
      (memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable).mp hfg'

Premises used: MeasureTheory.MemLp, MeasureTheory.memLp_add_of_disjoint, Iff.mp, MeasureTheory.SimpleFunc.stronglyMeasurable, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
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 : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
hg : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ), P (g.toLp hf)
hfg' : MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ
hf' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
hg' : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ
⊢ P ((f + g).toLp hfg')

Tactic:
add hf' hg' hfg (hf hf') (hg hg')

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.AEEqFun.comp₂, MeasureTheory.MemLp.toLp, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (simpleFunc.indicatorConst p (s := s) hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ)
    (hg : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ),
    Disjoint.{u_1} (α := Set α) (support.{u_1, u_4} (M := E) (⇑f : (a : α) → E))
        (support.{u_1, u_4} (M := E) (⇑g : (a : α) → E)) →
      P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
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 : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ), P (f.toLp hf)
hg : ∀ (hf : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ), P (g.toLp hf)
hfg' : MemLp.{u_1, u_4} (ε := E) (⇑(f + g) : (a : α) → E) p μ
hf' : MemLp.{u_1, u_4} (ε := E) (⇑f : (a : α) → E) p μ
hg' : MemLp.{u_1, u_4} (ε := E) (⇑g : (a : α) → E) p μ
⊢ P ((f + g).toLp hfg')

Tactic:
exact add hf' hg' hfg (hf hf') (hg hg')
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
⊢ UniformContinuous (α := ↥(simpleFunc E p μ))
    (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))

Tactic:
uniformContinuous_comap

Premises used: uniformContinuous_comap
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
⊢ IsUniformEmbedding (α := ↥(simpleFunc E p μ))
    (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))

Tactic:
isUniformEmbedding_comap Subtype.val_injective

Premises used: isUniformEmbedding_comap, Subtype.val_injective
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
⊢ IsUniformInducing (α := ↥(simpleFunc E p μ))
    (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))

Tactic:
simpleFunc.isUniformEmbedding.isUniformInducing

Premises used: IsUniformEmbedding.isUniformInducing, MeasureTheory.Lp.simpleFunc.isUniformEmbedding
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
apply :
  DenseRange (X := ↥(Lp E p μ)) (α := ↥(simpleFunc E p μ))
    (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))
⊢ IsDenseEmbedding (α := ↥(simpleFunc E p μ))
    (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))

Tactic:
apply simpleFunc.isUniformEmbedding.isDenseEmbedding

Premises used: IsUniformEmbedding.isDenseEmbedding, MeasureTheory.Lp.simpleFunc.isUniformEmbedding
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f : ↥(Lp E p μ)
rw :
  ∃ (x : ℕ → ↥(Lp E p μ)),
    (∀ (n : ℕ),
        Membership.mem (γ := Set ↥(Lp E p μ))
          (Set.range (ι := ↥(simpleFunc E p μ))
            (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦
              Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)))
          (x n)) ∧
      Tendsto x atTop (𝓝 f)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (Set.range (ι := ↥(simpleFunc E p μ))
        (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦
          Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x))))
    f

Tactic:
rw [mem_closure_iff_seq_limit]

Premises used: mem_closure_iff_seq_limit
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f : ↥(Lp E p μ)
⊢ MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ

Tactic:
have hfi' : MemLp f p μ := Lp.memLp f
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f : ↥(Lp E p μ)
hfi' : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ
⊢ SeparableSpace.{u_4} (↑(Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) : Type u_4)

Tactic:
haveI : SeparableSpace (range f ∪ {0} : Set E) :=
    (Lp.stronglyMeasurable f).separableSpace_range_union_singleton
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
f : ↥(Lp E p μ)
hfi' : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ
this : SeparableSpace.{u_4} (↑(Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) : Type u_4)
⊢ ∃ (x : ℕ → ↥(Lp E p μ)),
    (∀ (n : ℕ),
        Membership.mem (γ := Set ↥(Lp E p μ))
          (Set.range (ι := ↥(simpleFunc E p μ))
            (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦
              Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)))
          (x n)) ∧
      Tendsto x atTop (𝓝 f)

Tactic:
⟨fun n =>
      toLp
        (SimpleFunc.approxOn f (Lp.stronglyMeasurable f).measurable (range f ∪ {0}) 0 _ n)
        (SimpleFunc.memLp_approxOn_range (Lp.stronglyMeasurable f).measurable hfi' n),
      fun n => mem_range_self _, ?_⟩

Premises used: Set.mem_range_self, MeasureTheory.SimpleFunc.toLp, MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.AEEqFun.cast, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.SimpleFunc.memLp_approxOn_range, And.intro, MeasureTheory.SimpleFunc.approxOn, Exists.intro, Set.range, Union.union, Singleton.singleton, OfNat.ofNat, Subtype.val, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm._proof_1
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
f : ↥(Lp E p μ)
hfi' : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ
this : SeparableSpace.{u_4} (↑(Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) : Type u_4)
n :
  Tendsto
    (fun (n : ℕ) ↦
      (↑((approxOn (↑(↑f : α →ₘ[μ] E) : α → E) ⋯ (Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) 0 ⋯ n).toLp ⋯) :
        ↥(Lp E p μ)))
    atTop (𝓝 f)
⊢ ∃ (x : ℕ → ↥(Lp E p μ)),
    (∀ (n : ℕ),
        Membership.mem (γ := Set ↥(Lp E p μ))
          (Set.range (ι := ↥(simpleFunc E p μ))
            (Subtype.val (p := fun (x : ↥(Lp E p μ)) ↦
              Membership.mem (γ := AddSubgroup ↥(Lp E p μ)) (simpleFunc E p μ) x)))
          (x n)) ∧
      Tendsto x atTop (𝓝 f)

Tactic:
refine
    ⟨fun n =>
      toLp
        (SimpleFunc.approxOn f (Lp.stronglyMeasurable f).measurable (range f ∪ {0}) 0 _ n)
        (SimpleFunc.memLp_approxOn_range (Lp.stronglyMeasurable f).measurable hfi' n),
      fun n => mem_range_self _, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst_2 : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
f : ↥(Lp E p μ)
hfi' : MemLp (↑(↑f : α →ₘ[μ] E) : α → E) p μ
this : SeparableSpace.{u_4} (↑(Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) : Type u_4)
⊢ Tendsto
    (fun (n : ℕ) ↦
      MemLp.toLp
        (⇑(approxOn (↑(↑f : α →ₘ[μ] E) : α → E) ⋯ (Set.range (↑(↑f : α →ₘ[μ] E) : α → E) ∪ {0}) 0 ⋯ n) : (a : α) → E) ⋯)
    atTop (𝓝 (MemLp.toLp (↑(↑f : α →ₘ[μ] E) : α → E) hfi'))

Tactic:
SimpleFunc.tendsto_approxOn_range_Lp hp_ne_top (Lp.stronglyMeasurable f).measurable hfi'

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp