awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ < ∞
have rw : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
Tactic: rw [eLpNorm_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
have h : ∀ (x : β), f x - y₀ = HAdd.hAdd (β := β → E) f (-fun (x : β) ↦ y₀) x
Tactic: convert! eLpNorm_add_lt_top hf hi₀.neg with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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 : ℕ
⊢ eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
have hf' : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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₀‖‖
have h : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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₀‖‖
have h : ‖‖f x - y₀‖ + ‖f x - y₀‖‖ = ‖f x - y₀‖ + ‖f x - y₀‖
Tactic: convert! norm_approxOn_y₀_le fmeas h₀ x n using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 : β
⊢ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ = ‖f x - y₀‖ + ‖f x - y₀‖
have h : 0 ≤ ‖f x - y₀‖ + ‖f x - y₀‖
Tactic: rw [Real.norm_eq_abs, abs_of_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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 μ
⊢ eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
have this : ∀ᵐ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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)
have refine_1 : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
Tactic: refine tendsto_approxOn_Lp_eLpNorm fmeas _ hp_ne_top ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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})
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) : (a : β) → E) - f) p μ)
    atTop (𝓝 0)
have refine_2 : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - 0) p μ < ∞
Tactic: refine tendsto_approxOn_Lp_eLpNorm fmeas _ hp_ne_top ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
have refine_1 : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β | (fun (x : β) ↦ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})) x} a
Tactic: filter_upwards with x using subset_closure (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
have refine_1₁ : ∀ (a : β), f a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
Tactic: filter_upwards with x using subset_closure (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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
⊢ ∃ (g : β →ₛ E), eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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), eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
have 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 μ
Tactic: rsuffices ⟨g, hg, g_mem⟩ : ∃ g : β →ₛ E, eLpNorm (f' - ⇑g) p μ < ε ∧ MemLp g p μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 μ
⊢ ∃ (g : β →ₛ E), eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
have rsuffices₁ : ∃ (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 μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 μ
have refine : eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε
Tactic: refine ⟨g, ?_, g_mem⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 μ
⊢ eLpNorm (f - (⇑g : (a : β) → E)) p μ < ε
have suffices : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 μ
⊢ eLpNorm (f - (⇑g : (a : β) → E)) p μ = eLpNorm (f' - (⇑g : (a : β) → E)) p μ
have hfg : f - (⇑g : (a : β) → E) =ᶠ[ae μ] f' - (⇑g : (a : β) → E)
Tactic: apply eLpNorm_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 μ
⊢ f - (⇑g : (a : β) → E) =ᶠ[ae μ] f' - (⇑g : (a : β) → E)
have h : ∀ (x : β) (hx : f x = AEStronglyMeasurable.mk f sorry x),
  HSub.hSub (β := (a : β) → E) f (⇑g : (a : β) → E) x = HSub.hSub (β := (a : β) → E) f' (⇑g : (a : β) → E) x
Tactic: filter_upwards [hf.1.ae_eq_mk] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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), eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
have hf' : MemLp f' p μ
Tactic: have hf' : MemLp f' p μ := hf.ae_eq hf.1.ae_eq_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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 μ
⊢ ∃ (g : β →ₛ E), eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
have f'meas : Measurable f'
Tactic: have f'meas : Measurable f' := hf.1.measurable_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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'
⊢ ∃ (g : β →ₛ E), eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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)
⊢ ∃ (g : β →ₛ E), eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
have rcases : ∀ (n : ℕ) (hn : eLpNorm ((⇑(approxOn f' f'meas (Set.range f' ∪ {0}) 0 sorry n) : (a : β) → E) - f') 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
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 μ < ε
⊢ ∃ (g : β →ₛ E), eLpNorm (f' - (⇑g : (a : β) → E)) p μ < ε ∧ MemLp.{u_2, u_7} (ε := E) (⇑g : (a : β) → E) p μ
have hn₁ : eLpNorm (f' - (⇑(approxOn f' f'meas (Set.range f' ∪ {0}) 0 sorry n) : (a : β) → E)) p μ < ε
Tactic: rw [← eLpNorm_neg, neg_sub] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 : ℕ
⊢ Integrable.{u_4, u_2} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) μ
have 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 μ
Tactic: rw [← memLp_one_iff_integrable] at hf hi₀ ⊢
Cleared hypotheses: hf, s, y₀, h₀, inst_4, hi₀, n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 μ
⊢ 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)
have hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
Tactic: apply tendsto_approxOn_L1_enorm fmeas
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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})
⊢ 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)
have hi : HasFiniteIntegral.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - 0) μ
Tactic: apply tendsto_approxOn_L1_enorm fmeas
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
have hμ : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β | (fun (x : β) ↦ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})) x} a
Tactic: filter_upwards with x using subset_closure (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
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
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
have hμ₁ : ∀ (a : β), f a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
Tactic: filter_upwards with x using subset_closure (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
α : Type u_1
F : Type u_5
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ eLpNorm'.{u_1, u_5} (ε := F) (⇑f : (a : α) → F) p μ =
    HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
      (1 / p)
have h_map : Eq (α := α → ℝ≥0∞) (fun (x : α) ↦ enorm.{u_5} (E := F) ((f : (a : α) → F) x : F) ^ p)
  (⇑(map (fun (x : F) ↦ ‖x‖ₑ ^ p) f) : (a : α) → ℝ≥0∞)
Tactic: have h_map : (‖f ·‖ₑ ^ p) = f.map (‖·‖ₑ ^ p) := by simp; rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
F : Type u_5
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
h_map :
  Eq (α := α → ℝ≥0∞) (fun (x : α) ↦ enorm.{u_5} (E := F) ((f : (a : α) → F) x : F) ^ p)
    (⇑(map (fun (x : F) ↦ ‖x‖ₑ ^ p) f) : (a : α) → ℝ≥0∞)
⊢ eLpNorm'.{u_1, u_5} (ε := F) (⇑f : (a : α) → F) p μ =
    HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
      (1 / p)
have rw : (∫⁻ (a : α), enorm.{u_5} (E := F) ((f : (a : α) → F) a : F) ^ p ∂μ) ^ (1 / p) =
  HPow.hPow (α := ℝ≥0∞)
    (∑ y ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
    (1 / p)
Tactic: rw [eLpNorm'_eq_lintegral_enorm, h_map, lintegral_eq_lintegral, map_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
α : Type u_1
F : Type u_5
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
h_map :
  Eq (α := α → ℝ≥0∞) (fun (x : α) ↦ enorm.{u_5} (E := F) ((f : (a : α) → F) x : F) ^ p)
    (⇑(map (fun (x : F) ↦ ‖x‖ₑ ^ p) f) : (a : α) → ℝ≥0∞)
rw :
  (∫⁻ (a : α), enorm.{u_5} (E := F) ((f : (a : α) → F) a : F) ^ p ∂μ) ^ (1 / p) =
    HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
      (1 / p)
⊢ eLpNorm'.{u_1, u_5} (ε := F) (⇑f : (a : α) → F) p μ =
    HPow.hPow (α := ℝ≥0∞)
      (∑ y ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
      (1 / p)
have rw₁ : MeasureTheory.lintegral μ (⇑(map (fun (x : F) ↦ ‖x‖ₑ ^ p) f) : (a : α) → ℝ≥0∞) ^ (1 / p) =
  HPow.hPow (α := ℝ≥0∞)
    (∑ y ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (‖y‖ₑ ^ p) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) : ℝ≥0∞))
    (1 / p)
Tactic: rw [eLpNorm'_eq_lintegral_enorm, h_map, lintegral_eq_lintegral, map_lintegral]