-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem memLp_approxOn [BorelSpace E] {f : β → E} {μ : Measure β} (fmeas : Measurable f)
    (hf : MemLp f p μ) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s]
    (hi₀ : MemLp (fun _ => y₀) p μ) (n : ℕ) : MemLp (approxOn f fmeas s y₀ h₀ n) p μ

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
⊢ eLpNorm (⇑(approxOn f fmeas s y₀ h₀ n)) 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

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
⊢ eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ MemLp (fun x => ‖f x - y₀‖) p μ

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

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ eLpNorm (fun x => ‖f x - y₀‖) p μ < ⊤

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
this : ∀ᵐ (x : β) ∂μ, ‖(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
⊢ eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - 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'

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
x : β
⊢ f x - y₀ = (f + -fun x => y₀) x

Tactic:
simp [sub_eq_add_neg]

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ eLpNorm (fun x => f x - y₀) p μ < ⊤

Tactic:
convert eLpNorm_add_lt_top hf hi₀.neg with x

Result:
case h.e'_3.h.e'_5.h
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
x : β
⊢ f x - y₀ = (f + -fun x => y₀) x

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
this✝ : eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : MemLp (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ
⊢ eLpNorm (⇑(approxOn f fmeas s y₀ h₀ n)) p μ < ⊤

Tactic:
convert eLpNorm_add_lt_top this hi₀

Result:
case h.e'_3.h.e'_5
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
this✝ : eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : MemLp (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ
⊢ ⇑(approxOn f fmeas s y₀ h₀ n) = (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) + fun x => y₀

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
⊢ Measurable fun x => ‖f x - y₀‖

Tactic:
simp only [← dist_eq_norm]

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
⊢ Measurable fun x => dist (f x) y₀

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
⊢ MemLp (fun x => ‖f x - y₀‖) p μ

Tactic:
have h_meas : Measurable fun x => ‖f x - y₀‖ := by
  simp only [← dist_eq_norm]
  exact (continuous_id.dist continuous_const).measurable.comp fmeas

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ MemLp (fun x => ‖f x - y₀‖) p μ

Proof state:
case h.e'_3.h.e'_5
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
this✝ : eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : MemLp (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ
⊢ ⇑(approxOn f fmeas s y₀ h₀ n) = (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) + fun x => y₀

Tactic:
ext x

Result:
case h.e'_3.h.e'_5.h
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
this✝ : eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : MemLp (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ
x : β
⊢ (approxOn f fmeas s y₀ h₀ n) x = ((fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) + fun x => y₀) x