awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (hypothesis)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have hε₂' : 0 < ENNReal.ofReal (ε / 2)
Tactic: have hε₂' : 0 < ENNReal.ofReal (ε / 2) := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (g : E → F) (hg₁ : HasCompactSupport g) (hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)) (hg₃ : Continuous g)
  (hg₄ : MemLp g p μ), ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨g, hg₁, hg₂, hg₃, hg₄⟩ := hf.exists_hasCompactSupport_eLpNorm_sub_le hp hε₂'.ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (g' : E → F) (hg'₁ : HasCompactSupport g') (hg'₂ : ContDiff ℝ ∞ g')
  (hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)),
  ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨g', hg'₁, hg'₂, hg'₃⟩ := hg₁.exist_eLpNorm_sub_le_of_continuous μ hε₂ hg₃
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have refine : eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨g', hg'₁, hg'₂, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (hypothesis)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
⊢ eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε
have this : f - g' = f - g - (g' - g)
Tactic: have : f - g' = (f - g) - (g' - g) := by simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
this : f - g' = f - g - (g' - g)
⊢ eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε
have grw : eLpNorm (f - g - (g' - g)) p μ ≤ ENNReal.ofReal ε
Tactic: grw [this, eLpNorm_sub_le (hf.aestronglyMeasurable.sub hg₄.aestronglyMeasurable)
    (hg'₂.continuous.aestronglyMeasurable.sub hg₄.aestronglyMeasurable) hp₂, hg₂,
    eLpNorm_sub_comm, hg'₃, ← ENNReal.ofReal_add hε₂.le hε₂.le, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
this : f - g' = f - g - (g' - g)
grw : eLpNorm (f - g - (g' - g)) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε
have grw₁ : eLpNorm (f - g) p μ + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
Tactic: grw [this, eLpNorm_sub_le (hf.aestronglyMeasurable.sub hg₄.aestronglyMeasurable)
    (hg'₂.continuous.aestronglyMeasurable.sub hg₄.aestronglyMeasurable) hp₂, hg₂,
    eLpNorm_sub_comm, hg'₃, ← ENNReal.ofReal_add hε₂.le hε₂.le, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
this : f - g' = f - g - (g' - g)
grw : eLpNorm (f - g - (g' - g)) p μ ≤ ENNReal.ofReal ε
grw₁ : eLpNorm (f - g) p μ + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε
have grw₂ : ENNReal.ofReal (ε / 2) + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
Tactic: grw [this, eLpNorm_sub_le (hf.aestronglyMeasurable.sub hg₄.aestronglyMeasurable)
    (hg'₂.continuous.aestronglyMeasurable.sub hg₄.aestronglyMeasurable) hp₂, hg₂,
    eLpNorm_sub_comm, hg'₃, ← ENNReal.ofReal_add hε₂.le hε₂.le, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
this : f - g' = f - g - (g' - g)
grw : eLpNorm (f - g - (g' - g)) p μ ≤ ENNReal.ofReal ε
grw₁ : eLpNorm (f - g) p μ + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
grw₂ : ENNReal.ofReal (ε / 2) + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε
have grw₃ : ENNReal.ofReal (ε / 2) + eLpNorm (g - g') p μ ≤ ENNReal.ofReal ε
Tactic: grw [this, eLpNorm_sub_le (hf.aestronglyMeasurable.sub hg₄.aestronglyMeasurable)
    (hg'₂.continuous.aestronglyMeasurable.sub hg₄.aestronglyMeasurable) hp₂, hg₂,
    eLpNorm_sub_comm, hg'₃, ← ENNReal.ofReal_add hε₂.le hε₂.le, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
this : f - g' = f - g - (g' - g)
grw : eLpNorm (f - g - (g' - g)) p μ ≤ ENNReal.ofReal ε
grw₁ : eLpNorm (f - g) p μ + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
grw₂ : ENNReal.ofReal (ε / 2) + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
grw₃ : ENNReal.ofReal (ε / 2) + eLpNorm (g - g') p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε
have grw₄ : ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε
Tactic: grw [this, eLpNorm_sub_le (hf.aestronglyMeasurable.sub hg₄.aestronglyMeasurable)
    (hg'₂.continuous.aestronglyMeasurable.sub hg₄.aestronglyMeasurable) hp₂, hg₂,
    eLpNorm_sub_comm, hg'₃, ← ENNReal.ofReal_add hε₂.le hε₂.le, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
this : f - g' = f - g - (g' - g)
grw : eLpNorm (f - g - (g' - g)) p μ ≤ ENNReal.ofReal ε
grw₁ : eLpNorm (f - g) p μ + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
grw₂ : ENNReal.ofReal (ε / 2) + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
grw₃ : ENNReal.ofReal (ε / 2) + eLpNorm (g - g') p μ ≤ ENNReal.ofReal ε
grw₄ : ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε
⊢ eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε
have grw₅ : ENNReal.ofReal (ε / 2 + ε / 2) ≤ ENNReal.ofReal ε
Tactic: grw [this, eLpNorm_sub_le (hf.aestronglyMeasurable.sub hg₄.aestronglyMeasurable)
    (hg'₂.continuous.aestronglyMeasurable.sub hg₄.aestronglyMeasurable) hp₂, hg₂,
    eLpNorm_sub_comm, hg'₃, ← ENNReal.ofReal_add hε₂.le hε₂.le, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
this : f - g' = f - g - (g' - g)
grw : eLpNorm (f - g - (g' - g)) p μ ≤ ENNReal.ofReal ε
grw₁ : eLpNorm (f - g) p μ + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
grw₂ : ENNReal.ofReal (ε / 2) + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
grw₃ : ENNReal.ofReal (ε / 2) + eLpNorm (g - g') p μ ≤ ENNReal.ofReal ε
grw₄ : ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε
grw₅ : ENNReal.ofReal (ε / 2 + ε / 2) ≤ ENNReal.ofReal ε
⊢ eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε
have grw₆ : ENNReal.ofReal ε ≤ ENNReal.ofReal ε
Tactic: grw [this, eLpNorm_sub_le (hf.aestronglyMeasurable.sub hg₄.aestronglyMeasurable)
    (hg'₂.continuous.aestronglyMeasurable.sub hg₄.aestronglyMeasurable) hp₂, hg₂,
    eLpNorm_sub_comm, hg'₃, ← ENNReal.ofReal_add hε₂.le hε₂.le, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
⊢ Membership.mem (γ := Set ↥(Lp F p μ))
    (closure
      {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g})
    f
have refine : ∀ (ε : ℝ) (hε : 0 < ε),
  ∃ (y : ↥(Lp F p μ)),
    Membership.mem (γ := Set ↥(Lp F p μ))
        {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
        y ∧
      y ∈ Metric.closedBall f ε
Tactic: refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
⊢ ∃ (y : ↥(Lp F p μ)),
    Membership.mem (γ := Set ↥(Lp F p μ))
        {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
        y ∧
      y ∈ Metric.closedBall f ε
have obtain : ∀ (g : E → F) (hg₁ : HasCompactSupport g) (hg₂ : ContDiff ℝ ∞ g)
  (hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε),
  ∃ (y : ↥(Lp F p μ)),
    Membership.mem (γ := Set ↥(Lp F p μ))
        {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
        y ∧
      y ∈ Metric.closedBall f ε
Tactic: obtain ⟨g, hg₁, hg₂, hg₃⟩ := exist_eLpNorm_sub_le hp hp₂.out (Lp.memLp f) hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (hypothesis)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (y : ↥(Lp F p μ)),
    Membership.mem (γ := Set ↥(Lp F p μ))
        {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
        y ∧
      y ∈ Metric.closedBall f ε
have hg₄ : MemLp g p μ
Tactic: have hg₄ : MemLp g p μ := hg₂.continuous.memLp_of_hasCompactSupport hg₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
⊢ ∃ (y : ↥(Lp F p μ)),
    Membership.mem (γ := Set ↥(Lp F p μ))
        {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
        y ∧
      y ∈ Metric.closedBall f ε
have h : Membership.mem (γ := Set ↥(Lp F p μ))
    {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
    (toLp g hg₄) ∧
  toLp g hg₄ ∈ Metric.closedBall f ε
Tactic: use hg₄.toLp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
⊢ Membership.mem (γ := Set ↥(Lp F p μ))
      {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
      (toLp g hg₄) ∧
    toLp g hg₄ ∈ Metric.closedBall f ε
have right : toLp g hg₄ ∈ Metric.closedBall f ε
Tactic: use ⟨g, hg₄.coeFn_toLp, hg₁, hg₂⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
⊢ toLp g hg₄ ∈ Metric.closedBall f ε
have right : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F)) p μ ≤ ENNReal.ofReal ε
Tactic: rw [Metric.mem_closedBall, dist_comm, Lp.dist_def,
    ← le_ofReal_iff_toReal_le ((Lp.memLp f).sub (Lp.memLp hg₄.toLp)).eLpNorm_ne_top hε.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
⊢ eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F)) p μ ≤ ENNReal.ofReal ε
have h : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F)) p μ =
  eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ
Tactic: convert! hg₃ using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
⊢ eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F)) p μ =
    eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ
have h : (↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] (↑(↑f : E →ₘ[μ] F) : E → F) - g
Tactic: apply eLpNorm_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
⊢ (↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] (↑(↑f : E →ₘ[μ] F) : E → F) - g
have h : (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.WithLp (goal)
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : SMul K K'
inst_1 : SMul K V
inst_2 : SMul K' V
inst_3 : IsScalarTower K K' V
x : K
y : K'
z : WithLp p V
⊢ (x • y) • z = x • y • z
have change : toLp p ((x • y) • z.ofLp) = toLp p (x • y • z.ofLp)
Tactic: change toLp p ((x • y) • (ofLp z)) = toLp p (x • y • ofLp z)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.WithLp (goal)
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : SMul K V
inst_1 : SMul K' V
inst_2 : SMulCommClass K K' V
x : K
y : K'
z : WithLp p V
⊢ x • y • z = y • x • z
have change : toLp p (x • y • z.ofLp) = toLp p (y • x • z.ofLp)
Tactic: change toLp p (x • y • ofLp z) = toLp p (y • x • ofLp z)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.WithLp (goal)
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : SMul K V
inst_1 : SMul K' V
inst_2 : SMulCommClass K K' V
x : K
y : K'
z : WithLp p V
⊢ toLp p (x • y • z.ofLp) = toLp p (y • x • z.ofLp)
have rw : toLp p (y • x • z.ofLp) = toLp p (y • x • z.ofLp)
Tactic: rw [smul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ (if Eq (α := ℝ≥0∞) 0 0 then Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0}
    else Summable (α := ℝ) fun (i : α) ↦ HPow.hPow (β := ℝ) ‖f i‖ 0) ↔
    Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0}
have rw : Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0} ↔ Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0}
Tactic: rw [if_pos rfl]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : (i : α) → E i
⊢ Memℓp (E := E) f p ↔ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
have rw : ∀ (hp : 0 < p ∧ p < ∞) {f : (i : α) → E i}, Memℓp (E := E) f p ↔ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
Tactic: rw [ENNReal.toReal_pos_iff] at hp
Cleared hypotheses: hp, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ∞
f : (i : α) → E i
⊢ (if p = 0 then Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0}
    else
      if p = ∞ then BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
      else Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal) ↔
    Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
have rw : (if p = ∞ then BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
  else Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal) ↔
  Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
Tactic: rw [if_neg hp.1.ne', if_neg hp.2.ne]