awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
hf' : MemLp (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ
this :
  ∀ᵐ (x : β) ∂μ, ‖HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
⊢ eLpNorm (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖ + ‖f x - y₀‖) p μ < ∞

Tactic:
eLpNorm_add_lt_top hf' hf'

Premises used: MeasureTheory.eLpNorm_add_lt_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
hf' : MemLp (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ
this :
  ∀ᵐ (x : β) ∂μ, ‖HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
⊢ eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞

Tactic:
calc
    eLpNorm (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ ≤
        eLpNorm (fun x => ‖f x - y₀‖ + ‖f x - y₀‖) p μ :=
      eLpNorm_mono_ae this
    _ < ⊤ := eLpNorm_add_lt_top hf' hf'

Premises used: Norm.norm, MeasureTheory.eLpNorm_add_lt_top, MeasureTheory.eLpNorm_mono_ae, HSub.hSub, HAdd.hAdd, MeasureTheory.SimpleFunc.approxOn, DFunLike.coe, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst_4 : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst_5 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : eLpNorm f p μ < ∞
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : eLpNorm f p μ < ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) : (a : β) → E) - f) p μ)
    atTop (𝓝 0)

Tactic:
tendsto_approxOn_Lp_eLpNorm fmeas _ hp_ne_top ?_ ?_

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : eLpNorm f p μ < ∞
refine_1 : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
refine_2 : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - 0) p μ < ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) : (a : β) → E) - f) p μ)
    atTop (𝓝 0)

Tactic:
refine tendsto_approxOn_Lp_eLpNorm fmeas _ hp_ne_top ?_ ?_

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : eLpNorm f p μ < ∞
x : β
⊢ f x ∈ Set.range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : eLpNorm f p μ < ∞
refine_1 :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β | (fun (x : β) ↦ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})) x}
      a
refine_1₁ refine_1₂ : ∀ (x : β), f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})

Tactic:
filter_upwards with x using subset_closure (by simp)

Premises used: subset_closure
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : eLpNorm f p μ < ∞
⊢ eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - 0) p μ < ∞

Tactic:
simpa using hf
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst_4 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
inst_5 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : MemLp f p μ
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : MemLp f p μ
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst_4 : BorelSpace E
f : β → E
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst_5 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : MemLp f p μ
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
hf : MemLp f p μ
⊢ Tendsto (fun (n : ℕ) ↦ MemLp.toLp (⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) : (a : β) → E) ⋯) atTop
    (𝓝 (MemLp.toLp f hf))

Tactic:
simpa only [Lp.tendsto_Lp_iff_tendsto_eLpNorm''] using
    tendsto_approxOn_range_Lp_eLpNorm hp_ne_top fmeas hf.2

Premises used: MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'', And.right, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
rsuffices :
  ∀ (g : β →ₛ E) (hg : eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε)
    (g_mem : MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ),
    ∃ (g : β →ₛ E), eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
rsuffices₁ :
  ∃ (g : β →ₛ E), eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
⊢ ∃ (g : β →ₛ E), eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ

Tactic:
rsuffices ⟨g, hg, g_mem⟩ : ∃ g : β →ₛ E, eLpNorm (f' - ⇑g) p μ < ε ∧ MemLp g p μ
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
g : β →ₛ E
hg : eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε
g_mem : MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
⊢ ∃ (g : β →ₛ E), eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ

Tactic:
⟨g, ?_, g_mem⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
g : β →ₛ E
hg : eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε
g_mem : MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
refine : eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε
⊢ ∃ (g : β →ₛ E), eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ

Tactic:
refine ⟨g, ?_, g_mem⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
g : β →ₛ E
hg : eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε
g_mem : MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
this : eLpNorm (f - (⇑g : (a : β) → E)) p μ = eLpNorm (f' - (⇑g : (a : β) → E)) p μ
rwa rwa₁ rwa₂ rwa₃ : eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε
⊢ eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε

Tactic:
rwa [this]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
g : β →ₛ E
hg : eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε
g_mem : MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
suffices : eLpNorm (f - (⇑g : (a : β) → E)) p μ = eLpNorm (f' - (⇑g : (a : β) → E)) p μ
⊢ eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε

Tactic:
suffices eLpNorm (f - ⇑g) p μ = eLpNorm (f' - ⇑g) p μ by rwa [this]
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
g : β →ₛ E
hg : eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε
g_mem : MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
hfg : f - (⇑g : (a : β) → E) =ᶠ[ae μ] f' - (⇑g : (a : β) → E)
⊢ eLpNorm (f - (⇑g : (a : β) → E)) p μ = eLpNorm (f' - (⇑g : (a : β) → E)) p μ

Tactic:
apply eLpNorm_congr_ae

Premises used: MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
g : β →ₛ E
hg : eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε
g_mem : MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
h :
  ∀ (x : β) (hx : f x = AEStronglyMeasurable.mk f ⋯ x),
    HSub.hSub (β := (a : β) → E) f (⇑g : (a : β) → E) x = HSub.hSub (β := (a : β) → E) f' (⇑g : (a : β) → E) x
⊢ f - (⇑g : (a : β) → E) =ᶠ[ae μ] f' - (⇑g : (a : β) → E)

Tactic:
filter_upwards [hf.1.ae_eq_mk] with x hx

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
g : β →ₛ E
hg : eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε
g_mem : MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
x : β
hx : f x = AEStronglyMeasurable.mk f ⋯ x
⊢ HSub.hSub (β := (a : β) → E) f (⇑g : (a : β) → E) x = HSub.hSub (β := (a : β) → E) f' (⇑g : (a : β) → E) x

Tactic:
simpa only [Pi.sub_apply, sub_left_inj] using hx

Premises used: sub_left_inj, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
⊢ MemLp f' p μ

Tactic:
have hf' : MemLp f' p μ := hf.ae_eq hf.1.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
hf' : MemLp f' p μ
⊢ Measurable f'

Tactic:
have f'meas : Measurable f' := hf.1.measurable_mk
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
hf' : MemLp f' p μ
f'meas : Measurable f'
⊢ SeparableSpace.{u_7} (↑(Set.range f' ∪ {0}) : Type u_7)

Tactic:
have : SeparableSpace (range f' ∪ {0} : Set E) :=
    StronglyMeasurable.separableSpace_range_union_singleton hf.1.stronglyMeasurable_mk
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
hf' : MemLp f' p μ
f'meas : Measurable f'
this : SeparableSpace.{u_7} (↑(Set.range f' ∪ {0}) : Type u_7)
rcases :
  ∀ (n : ℕ) (hn : eLpNorm ((⇑(approxOn f' f'meas (Set.range f' ∪ {0}) 0 ⋯ n) : (a : β) → E) - f') p μ < ε),
    ∃ (g : β →ₛ E), eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
⊢ ∃ (g : β →ₛ E), eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ

Tactic:
rcases ((tendsto_approxOn_range_Lp_eLpNorm hp_ne_top f'meas hf'.2).eventually <|
    gt_mem_nhds hε.bot_lt).exists with ⟨n, hn⟩

Premises used: gt_mem_nhds, Filter.Eventually.exists, And.right, Filter.Tendsto.eventually, Ne.bot_lt, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
hf' : MemLp f' p μ
f'meas : Measurable f'
this : SeparableSpace.{u_7} (↑(Set.range f' ∪ {0}) : Type u_7)
n : ℕ
hn : eLpNorm ((⇑(approxOn f' f'meas (Set.range f' ∪ {0}) 0 ⋯ n) : (a : β) → E) - f') p μ < ε
⊢ eLpNorm (f' - (⇑(approxOn f' f'meas (Set.range f' ∪ {0}) 0 ⋯ n) : (a : β) → E)) p μ < ε

Tactic:
rw [← eLpNorm_neg, neg_sub] at hn

Premises used: neg_sub, MeasureTheory.eLpNorm_neg
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
hf' : MemLp f' p μ
f'meas : Measurable f'
this : SeparableSpace.{u_7} (↑(Set.range f' ∪ {0}) : Type u_7)
n : ℕ
hn : eLpNorm (f' - (⇑(approxOn f' f'meas (Set.range f' ∪ {0}) 0 ⋯ n) : (a : β) → E)) p μ < ε
⊢ ∃ (g : β →ₛ E), eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ

Tactic:
⟨_, hn, memLp_approxOn_range f'meas hf' _⟩

Premises used: MeasureTheory.SimpleFunc.memLp_approxOn_range, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
inst : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst_1 : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
hf' : MemLp f' p μ
f'meas : Measurable f'
this : SeparableSpace.{u_7} (↑(Set.range f' ∪ {0}) : Type u_7)
n : ℕ
hn : eLpNorm (f' - (⇑(approxOn f' f'meas (Set.range f' ∪ {0}) 0 ⋯ n) : (a : β) → E)) p μ < ε
⊢ ∃ (g : β →ₛ E), eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ

Tactic:
exact ⟨_, hn, memLp_approxOn_range f'meas hf' _⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : HasFiniteIntegral.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) μ
⊢ eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) 1 μ < ∞

Tactic:
simpa [eLpNorm_one_eq_lintegral_enorm] using hi

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : HasFiniteIntegral.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) μ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ∂μ) atTop
    (𝓝 0)

Tactic:
simpa [eLpNorm_one_eq_lintegral_enorm] using
    tendsto_approxOn_Lp_eLpNorm hf h₀ one_ne_top hμ
      (by simpa [eLpNorm_one_eq_lintegral_enorm] using hi)

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm, MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Integrable f μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : Integrable.{u_4, u_2} (ε := E) (fun (x : β) ↦ y₀) μ
n : ℕ
rw :
  ∀ (hf : MemLp f 1 μ) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [inst_5 : SeparableSpace.{u_4} (↑s : Type u_4)]
    (hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) 1 μ) (n : ℕ),
    MemLp.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) 1 μ
⊢ Integrable.{u_4, u_2} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hi₀ ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f 1 μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) 1 μ
n : ℕ
⊢ MemLp.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) 1 μ

Tactic:
memLp_approxOn fmeas hf h₀ hi₀ n

Premises used: MeasureTheory.SimpleFunc.memLp_approxOn
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f 1 μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) 1 μ
n : ℕ
⊢ MemLp.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) 1 μ

Tactic:
exact memLp_approxOn fmeas hf h₀ hi₀ n

Premises used: MeasureTheory.SimpleFunc.memLp_approxOn
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
fmeas : Measurable f
hf : Integrable f μ
n : ℕ
x : β
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
fmeas : Measurable f
hf : Integrable f μ
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
hi : HasFiniteIntegral.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - 0) μ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n : (a : β) → E) x : E) (f x)‖ₑ ∂μ)
    atTop (𝓝 0)

Tactic:
apply tendsto_approxOn_L1_enorm fmeas

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn_L1_enorm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
fmeas : Measurable f
hf : Integrable f μ
x : β
⊢ f x ∈ Set.range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst_4 : SeparableSpace.{u_4} (↑(Set.range f ∪ {0}) : Type u_4)
fmeas : Measurable f
hf : Integrable f μ
hμ :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β | (fun (x : β) ↦ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})) x}
      a
hμ₁ hμ₂ : ∀ (x : β), f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})

Tactic:
filter_upwards with x using subset_closure (by simp)

Premises used: subset_closure