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 : 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))
h : 0 = (↑‖f a - f a‖₊ : ℝ≥0∞) ^ p.toReal
⊢ 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:
convert! 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
-- 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))
⊢ 0 = (↑‖f a - f a‖₊ : ℝ≥0∞) ^ p.toReal

Tactic:
simp [zero_rpow_of_pos hp]

Premises used: ENNReal.zero_rpow_of_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
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 : β) ∂μ,
    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:
have h_lim :
    ∀ᵐ a : β ∂μ, Tendsto (‖approxOn f hf s y₀ h₀ · a - f a‖ₑ ^ p.toReal) atTop (𝓝 0) := by
    filter_upwards [hμ] with a ha
    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
    convert! continuous_rpow_const.continuousAt.tendsto.comp (tendsto_coe.mpr this.nnnorm)
    simp [zero_rpow_of_pos 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
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_lim :
  ∀ᵐ (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)
⊢ 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)

Tactic:
simpa using tendsto_lintegral_of_dominated_convergence _ hF_meas h_bound h_fin h_lim

Premises used: MeasureTheory.tendsto_lintegral_of_dominated_convergence
-- 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 : ℕ
⊢ MemLp.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) p μ

Tactic:
⟨(approxOn f fmeas s y₀ h₀ n).aestronglyMeasurable, ?_⟩

Premises used: MeasureTheory.MemLp, And.intro, MeasureTheory.SimpleFunc.approxOn, MeasureTheory.SimpleFunc.aestronglyMeasurable
-- 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 : ℕ
refine : eLpNorm.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) p μ < ∞
⊢ MemLp.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) p μ

Tactic:
refine ⟨(approxOn f fmeas s y₀ h₀ n).aestronglyMeasurable, ?_⟩
-- 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 : ℕ
this :
  eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
⊢ MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p μ

Tactic:
have : MemLp (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ :=
      ⟨(approxOn f fmeas s y₀ h₀ n - const β y₀).aestronglyMeasurable, this⟩
-- 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 : ℕ
this_1 :
  eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
this :
  MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p μ
⊢ eLpNorm
      (HAdd.hAdd (α := β → E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀)
        fun (x : β) ↦ y₀)
      p μ <
    ∞

Tactic:
eLpNorm_add_lt_top this hi₀

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 : ℕ
this_1 :
  eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
this :
  MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p μ
h :
  (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) =
    HAdd.hAdd (α := β → E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀)
      fun (x : β) ↦ y₀
⊢ eLpNorm.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) p μ < ∞

Tactic:
convert! eLpNorm_add_lt_top this hi₀

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 : ℕ
this_1 :
  eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
this :
  MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p μ
h :
  ∀ (x : β),
    (approxOn f fmeas s y₀ h₀ n : (a : β) → E) x =
      HAdd.hAdd (α := β → E) (β := β → E)
        (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) (fun (x : β) ↦ y₀) x
⊢ (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) =
    HAdd.hAdd (α := β → E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀)
      fun (x : β) ↦ y₀

Tactic:
ext x
-- 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 : ℕ
this_1 :
  eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
this :
  MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p μ
x : β
⊢ (approxOn f fmeas s y₀ h₀ n : (a : β) → E) x =
    HAdd.hAdd (α := β → E) (β := β → E)
      (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) (fun (x : β) ↦ y₀) x

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
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 : ℕ
suffices :
  eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
⊢ eLpNorm.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) p μ < ∞

Tactic:
suffices eLpNorm (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ < ⊤ by
    have : MemLp (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ :=
      ⟨(approxOn f fmeas s y₀ h₀ n - const β y₀).aestronglyMeasurable, this⟩
    convert! eLpNorm_add_lt_top this hi₀
    ext x
    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
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 : ℕ
simp : Measurable (β := ℝ) fun (x : β) ↦ dist (f x) y₀
⊢ Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖

Tactic:
simp only [← dist_eq_norm]

Premises used: dist_eq_norm
-- 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 : ℕ
funProp : inst_1 ≤ inst_1
funProp₁ : MeasurableEmbedding (β := ℝ) fun (x2 : E) ↦ dist x2 y₀
⊢ Measurable (β := ℝ) fun (x : β) ↦ dist (f x) y₀

Tactic:
fun_prop
-- 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 : ℕ
⊢ Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖

Tactic:
have h_meas : Measurable fun x => ‖f x - y₀‖ := by
      simp only [← dist_eq_norm]
      fun_prop
-- 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 : ℕ
h_meas : Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖
⊢ MemLp (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ

Tactic:
⟨h_meas.aemeasurable.aestronglyMeasurable, ?_⟩

Premises used: AEMeasurable.aestronglyMeasurable, Measurable.aemeasurable, MeasureTheory.MemLp, And.intro
-- 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 : ℕ
h_meas : Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖
refine : eLpNorm (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ < ∞
⊢ MemLp (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ

Tactic:
refine ⟨h_meas.aemeasurable.aestronglyMeasurable, ?_⟩
-- 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 : ℕ
h_meas : Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖
rw : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ < ∞

Tactic:
rw [eLpNorm_norm]

Premises used: MeasureTheory.eLpNorm_norm
-- 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 : ℕ
h_meas : Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖
⊢ eLpNorm (f + -fun (x : β) ↦ y₀) p μ < ∞

Tactic:
eLpNorm_add_lt_top hf hi₀.neg

Premises used: MeasureTheory.eLpNorm_add_lt_top, MeasureTheory.MemLp.neg
-- 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 : ℕ
h_meas : Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖
h : ∀ (x : β), f x - y₀ = HAdd.hAdd (β := β → E) f (-fun (x : β) ↦ y₀) x
⊢ eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞

Tactic:
convert! eLpNorm_add_lt_top hf hi₀.neg with x

Premises used: MeasureTheory.eLpNorm_add_lt_top, MeasureTheory.MemLp.neg
-- 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 : ℕ
h_meas : Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖
x : β
⊢ f x - y₀ = HAdd.hAdd (β := β → E) f (-fun (x : β) ↦ y₀) x

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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 : ℕ
⊢ MemLp (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ

Tactic:
have hf' : MemLp (fun x => ‖f x - y₀‖) p μ := by
    have h_meas : Measurable fun x => ‖f x - y₀‖ := by
      simp only [← dist_eq_norm]
      fun_prop
    refine ⟨h_meas.aemeasurable.aestronglyMeasurable, ?_⟩
    rw [eLpNorm_norm]
    convert! eLpNorm_add_lt_top hf hi₀.neg with x
    simp [sub_eq_add_neg]
-- 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 μ
h : ∀ (x : β), ‖HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
⊢ ∀ᵐ (x : β) ∂μ, ‖HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖

Tactic:
filter_upwards with x
-- 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 μ
x : β
⊢ ‖HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖

Tactic:
norm_approxOn_y₀_le fmeas h₀ x n

Premises used: MeasureTheory.SimpleFunc.norm_approxOn_y₀_le
-- 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 μ
x : β
h : ‖‖f x - y₀‖ + ‖f x - y₀‖‖ = ‖f x - y₀‖ + ‖f x - y₀‖
⊢ ‖HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖

Tactic:
convert! norm_approxOn_y₀_le fmeas h₀ x n using 1

Premises used: MeasureTheory.SimpleFunc.norm_approxOn_y₀_le
-- 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 μ
x : β
h : 0 ≤ ‖f x - y₀‖ + ‖f x - y₀‖
⊢ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ = ‖f x - y₀‖ + ‖f x - y₀‖

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg]

Premises used: abs_of_nonneg, Real.norm_eq_abs
-- 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 μ
x : β
⊢ 0 ≤ ‖f x - y₀‖ + ‖f x - y₀‖

Tactic:
positivity
-- 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 μ
⊢ ∀ᵐ (x : β) ∂μ, ‖HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖

Tactic:
have : ∀ᵐ x ∂μ, ‖approxOn f fmeas s y₀ h₀ n x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ := by
    filter_upwards with x
    convert! norm_approxOn_y₀_le fmeas h₀ x n using 1
    rw [Real.norm_eq_abs, abs_of_nonneg]
    positivity
-- 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
      μ ≤
    eLpNorm (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖ + ‖f x - y₀‖) p μ

Tactic:
eLpNorm_mono_ae this

Premises used: MeasureTheory.eLpNorm_mono_ae