awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : (n : ℕ) → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n : (a : X × Y) → α) x) < u n
x : X × Y
n : ℕ
⊢ dist (f x) ((g n : (a : X × Y) → α) x) ≤ u n

Tactic:
(hg n x).le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : (n : ℕ) → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n : (a : X × Y) → α) x) < u n
x : X × Y
n : ℕ
⊢ dist (f x) ((g n : (a : X × Y) → α) x) ≤ u n

Tactic:
exact (hg n x).le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : (n : ℕ) → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n : (a : X × Y) → α) x) < u n
⊢ ∀ (x : X × Y), Tendsto (fun (n : ℕ) ↦ (g n : (a : X × Y) → α) x) atTop (𝓝 (f x))

Tactic:
have A : ∀ x, Tendsto (fun n ↦ g n x) atTop (𝓝 (f x)) := by
    intro x
    rw [tendsto_iff_dist_tendsto_zero]
    apply squeeze_zero (fun n ↦ dist_nonneg) (fun n ↦ ?_) u_lim
    rw [dist_comm]
    exact (hg n x).le
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : (n : ℕ) → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n : (a : X × Y) → α) x) < u n
A : ∀ (x : X × Y), Tendsto (fun (n : ℕ) ↦ (g n : (a : X × Y) → α) x) atTop (𝓝 (f x))
⊢ Measurable f

Tactic:
apply measurable_of_tendsto_metrizable (fun n ↦ (g n).measurable) (tendsto_pi_nhds.2 A)

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.measurable, tendsto_pi_nhds, measurable_of_tendsto_metrizable
-- 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)
x : β
n : ℕ
⊢ edist ((approxOn f hf s y₀ h₀ n : (a : β) → E) x) (f x) ≤ edist y₀ (f x)

Tactic:
have := edist_approxOn_le hf h₀ x n
-- 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)
x : β
n : ℕ
this : edist ((approxOn f hf s y₀ h₀ n : (a : β) → E) x) (f x) ≤ edist y₀ (f x)
⊢ edist ((approxOn f hf s y₀ h₀ n : (a : β) → E) x) (f x) ≤ edist (f x) y₀

Tactic:
rw [edist_comm y₀] at this

Premises used: PseudoEMetricSpace.edist_comm
-- 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)
x : β
n : ℕ
this : edist ((approxOn f hf s y₀ h₀ n : (a : β) → E) x) (f x) ≤ edist (f x) y₀
⊢ (↑‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖₊ : ℝ≥0∞) ≤ (↑‖f x - y₀‖₊ : ℝ≥0∞)

Tactic:
simp only [edist_nndist, nndist_eq_nnnorm] at this

Premises used: nndist_eq_nnnorm, edist_nndist
-- 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)
x : β
n : ℕ
this : (↑‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖₊ : ℝ≥0∞) ≤ (↑‖f x - y₀‖₊ : ℝ≥0∞)
⊢ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖₊ ≤ ‖f x - y₀‖₊

Tactic:
mod_cast this

Premises used: cast, ENNReal.coe_le_coe._simp_1
-- 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)
x : β
n : ℕ
this : (↑‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖₊ : ℝ≥0∞) ≤ (↑‖f x - y₀‖₊ : ℝ≥0∞)
⊢ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖₊ ≤ ‖f x - y₀‖₊

Tactic:
exact mod_cast this
-- 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)
x : β
n : ℕ
⊢ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖

Tactic:
simpa [enorm, edist_eq_enorm_sub, ← ENNReal.coe_add, norm_sub_rev]
    using edist_approxOn_y0_le hf h₀ x n

Premises used: edist_eq_enorm_sub, MeasureTheory.SimpleFunc.edist_approxOn_y0_le, ENNReal.coe_add, ENorm.enorm, norm_sub_rev
-- 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
h₀ : 0 ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
x : β
n : ℕ
⊢ norm.{u_4} (E := E) ((approxOn f hf s 0 h₀ n : (a : β) → E) x : E) ≤ ‖f x‖ + ‖f x‖

Tactic:
simpa [enorm, edist_eq_enorm_sub, ← ENNReal.coe_add, norm_sub_rev]
    using edist_approxOn_y0_le hf h₀ x n

Premises used: edist_eq_enorm_sub, MeasureTheory.SimpleFunc.edist_approxOn_y0_le, ENNReal.coe_add, ENorm.enorm, norm_sub_rev
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
pos :
  ∀ (hp_zero : p = 0),
    Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)
neg :
  ∀ (hp_zero : ¬p = 0),
    Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)

Tactic:
by_cases hp_zero : p = 0
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : p = 0
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)

Tactic:
simpa only [hp_zero, eLpNorm_exponent_zero] using tendsto_const_nhds

Premises used: tendsto_const_nhds, MeasureTheory.eLpNorm_exponent_zero
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
⊢ 0 < p.toReal

Tactic:
have hp : 0 < p.toReal := toReal_pos hp_zero hp_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
p : ℝ≥0∞
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)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
this :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
simp :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      (∫⁻ (x : β), ‖HSub.hSub (α := (a : β) → E) (⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) f x‖ₑ ^ p.toReal ∂μ) ^
        (1 / p.toReal))
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)

Tactic:
simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_ne_top]

Premises used: MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
this :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
⊢ Tendsto (α := ℕ)
    ((fun (a : ℝ≥0∞) ↦ a ^ (1 / p.toReal)) ∘ fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 (HPow.hPow (α := ℝ≥0∞) 0 (1 / p.toReal)))

Tactic:
continuous_rpow_const.continuousAt.tendsto.comp this

Premises used: Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp, ENNReal.continuous_rpow_const
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
this :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
h : 0 = HPow.hPow (α := ℝ≥0∞) 0 (1 / p.toReal)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      (∫⁻ (x : β), ‖HSub.hSub (α := (a : β) → E) (⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) f x‖ₑ ^ p.toReal ∂μ) ^
        (1 / p.toReal))
    atTop (𝓝 0)

Tactic:
convert! continuous_rpow_const.continuousAt.tendsto.comp this

Premises used: Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp, ENNReal.continuous_rpow_const
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
this :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
⊢ 0 = HPow.hPow (α := ℝ≥0∞) 0 (1 / p.toReal)

Tactic:
simp [zero_rpow_of_pos (_root_.inv_pos.mpr hp)]

Premises used: Iff.mpr, ENNReal.zero_rpow_of_pos, inv_pos
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
neg :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)

Tactic:
suffices Tendsto (fun n => ∫⁻ x, ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0) by
    simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_ne_top]
    convert! continuous_rpow_const.continuousAt.tendsto.comp this
    simp [zero_rpow_of_pos (_root_.inv_pos.mpr hp)]
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
n : ℕ
⊢ Measurable (β := ℝ≥0∞) fun (x : β) ↦
    ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal

Tactic:
simpa only [← edist_eq_enorm_sub] using
      (approxOn f hf s y₀ h₀ n).measurable_bind (fun y x => edist y (f x) ^ p.toReal) fun y =>
        (measurable_edist_right.comp hf).pow_const p.toReal

Premises used: edist_eq_enorm_sub, MeasureTheory.SimpleFunc.measurable_bind, Measurable.comp, measurable_edist_right, ENNReal.toReal, HPow.hPow, MeasureTheory.SimpleFunc.approxOn, EDist.edist, Measurable.pow_const
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
⊢ ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal

Tactic:
have hF_meas n : Measurable fun x => ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal := by
    simpa only [← edist_eq_enorm_sub] using
      (approxOn f hf s y₀ h₀ n).measurable_bind (fun y x => edist y (f x) ^ p.toReal) fun y =>
        (measurable_edist_right.comp hf).pow_const p.toReal
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
⊢ ∀ (n : ℕ),
    (ae μ).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal)
      fun (x : β) ↦ ‖f x - y₀‖ₑ ^ p.toReal

Tactic:
have h_bound n :
    (fun x ↦ ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal) ≤ᵐ[μ] (‖f · - y₀‖ₑ ^ p.toReal) :=
    .of_forall fun x => rpow_le_rpow (coe_mono (nnnorm_approxOn_le hf h₀ x n)) toReal_nonneg
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
h_bound :
  ∀ (n : ℕ),
    (ae μ).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal)
      fun (x : β) ↦ ‖f x - y₀‖ₑ ^ p.toReal
⊢ ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞

Tactic:
have h_fin : (∫⁻ a : β, ‖f a - y₀‖ₑ ^ p.toReal ∂μ) ≠ ⊤ :=
    (lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_ne_top hi).ne
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
h_bound :
  ∀ (n : ℕ),
    (ae μ).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal)
      fun (x : β) ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
h :
  ∀ (a : β) (ha : f a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
    Tendsto (β := ℝ≥0∞)
      (fun (x : ℕ) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ x : (a : β) → E) a : E) (f a)‖ₑ ^ p.toReal) atTop (𝓝 0)
⊢ ∀ᵐ (a : β) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (x : ℕ) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ x : (a : β) → E) a : E) (f a)‖ₑ ^ p.toReal) atTop (𝓝 0)

Tactic:
filter_upwards [hμ] with a ha
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
h_bound :
  ∀ (n : ℕ),
    (ae μ).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal)
      fun (x : β) ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
a : β
ha : f a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun (n : ℕ) ↦ HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) a : E) (f a)) atTop (𝓝 (f a - f a))

Tactic:
have : Tendsto (fun n => (approxOn f hf s y₀ h₀ n) a - f a) atTop (𝓝 (f a - f a)) :=
      (tendsto_approxOn hf h₀ ha).sub tendsto_const_nhds
-- 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 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
h_bound :
  ∀ (n : ℕ),
    (ae μ).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal)
      fun (x : β) ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
a : β
ha : f a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
this :
  Tendsto (fun (n : ℕ) ↦ HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) a : E) (f a)) atTop (𝓝 (f a - f a))
⊢ Tendsto (α := ℕ)
    ((fun (a : ℝ≥0∞) ↦ a ^ p.toReal) ∘ fun (a_1 : ℕ) ↦
      (↑‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ a_1 : (a : β) → E) a : E) (f a)‖₊ : ℝ≥0∞))
    atTop (𝓝 ((↑‖f a - f a‖₊ : ℝ≥0∞) ^ p.toReal))

Tactic:
continuous_rpow_const.continuousAt.tendsto.comp (tendsto_coe.mpr this.nnnorm)

Premises used: Iff.mpr, Continuous.continuousAt, ENNReal.tendsto_coe, ContinuousAt.tendsto, Filter.Tendsto.comp, ENNReal.continuous_rpow_const, Filter.Tendsto.nnnorm