awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
x x_1 : WithLp p (WithLp p (α × β) × γ)
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x x_2 : WithLp 0 (WithLp 0 (α × β) × γ)),
    edist (α := WithLp 0 (α × WithLp 0 (β × γ)))
        ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
            (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
          x)
        ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
            (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
          x_2) =
      edist x x_2
inr :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x x_2 : WithLp ∞ (WithLp ∞ (α × β) × γ)),
    edist (α := WithLp ∞ (α × WithLp ∞ (β × γ)))
        ((fun (x : WithLp ∞ (WithLp ∞ (α × β) × γ)) ↦
            (WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd)) : WithLp ∞ (α × WithLp ∞ (β × γ))))
          x)
        ((fun (x : WithLp ∞ (WithLp ∞ (α × β) × γ)) ↦
            (WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd)) : WithLp ∞ (α × WithLp ∞ (β × γ))))
          x_2) =
      edist x x_2
inr₁ :
  ∀ (hp_1 : 0 < p.toReal),
    edist (α := WithLp p (α × WithLp p (β × γ)))
        ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x)
        ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd)))
          x_1) =
      edist x x_1
⊢ edist (α := WithLp p (α × WithLp p (β × γ)))
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x)
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x_1) =
    edist x x_1

Tactic:
rcases p.trichotomy with rfl | rfl | hp

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
x x_1 : WithLp 0 (WithLp 0 (α × β) × γ)
⊢ ¬?_mvar.436370

Tactic:
hp.elim

Premises used: Fact.elim
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
x x_1 : WithLp 0 (WithLp 0 (α × β) × γ)
inl : ¬LE.le (α := ℝ≥0∞) 1 0
⊢ edist (α := WithLp 0 (α × WithLp 0 (β × γ)))
      ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
          (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
        x)
      ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
          (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
        x_1) =
    edist x x_1

Tactic:
absurd hp.elim

Premises used: Fact.elim
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
x x_1 : WithLp 0 (WithLp 0 (α × β) × γ)
⊢ ¬LE.le (α := ℝ≥0∞) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x x_1 : WithLp ∞ (WithLp ∞ (α × β) × γ)
⊢ edist (α := WithLp ∞ (α × WithLp ∞ (β × γ)))
      ((fun (x : WithLp ∞ (WithLp ∞ (α × β) × γ)) ↦
          (WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd)) : WithLp ∞ (α × WithLp ∞ (β × γ))))
        x)
      ((fun (x : WithLp ∞ (WithLp ∞ (α × β) × γ)) ↦
          (WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd)) : WithLp ∞ (α × WithLp ∞ (β × γ))))
        x_1) =
    edist x x_1

Tactic:
simp [WithLp.prod_edist_eq_sup, max_assoc]

Premises used: WithLp.prod_edist_eq_sup, max_assoc
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
x x_1 : WithLp p (WithLp p (α × β) × γ)
hp : 0 < p.toReal
⊢ edist (α := WithLp p (α × WithLp p (β × γ)))
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x)
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x_1) =
    edist x x_1

Tactic:
simp [WithLp.prod_edist_eq_add hp, ENNReal.rpow_inv_rpow hp.ne', add_assoc]

Premises used: ENNReal.rpow_inv_rpow, add_assoc, LT.lt.ne', WithLp.prod_edist_eq_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x y : WithLp 0 (α × β)), edist x.fst y.fst = edist x y
inr : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ (α × β)), edist x.fst y.fst = edist x y
inr₁ : ∀ (hp : 0 < p.toReal), edist x.fst y.fst = edist x y
⊢ edist x.fst y.fst = edist x y

Tactic:
rcases p.trichotomy with rfl | rfl | hp

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
__spread.0 : WithLp 0 (α × β) ≃ α := Equiv.trans (WithLp.equiv 0 (α × β)) (Equiv.prodUnique α β)
x y : WithLp 0 (α × β)
⊢ ¬?_mvar.458822

Tactic:
hp.elim

Premises used: Fact.elim
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
__spread.0 : WithLp 0 (α × β) ≃ α := Equiv.trans (WithLp.equiv 0 (α × β)) (Equiv.prodUnique α β)
x y : WithLp 0 (α × β)
inl : ¬LE.le (α := ℝ≥0∞) 1 0
⊢ edist x.fst y.fst = edist x y

Tactic:
absurd hp.elim

Premises used: Fact.elim
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
__spread.0 : WithLp 0 (α × β) ≃ α := Equiv.trans (WithLp.equiv 0 (α × β)) (Equiv.prodUnique α β)
x y : WithLp 0 (α × β)
⊢ ¬LE.le (α := ℝ≥0∞) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
inr : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
inr₁ :
  edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist.{u_3} (α := β) default default ^ p.toReal) ^ (1 / p.toReal)
inr₂ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + HPow.hPow (α := ℝ≥0∞) 0 p.toReal) ^ (1 / p.toReal)
inr₃ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + 0) ^ (1 / p.toReal)
inr₄ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal) ^ (1 / p.toReal)
inr₅ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal) ^ p.toReal⁻¹
⊢ edist x.fst y.fst = edist x y

Tactic:
simp_rw [WithLp.prod_edist_eq_add hp, Unique.eq_default, edist_self,
        ENNReal.zero_rpow_of_pos hp, add_zero, one_div, ENNReal.rpow_rpow_inv hp.ne']

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.rpow_rpow_inv, PseudoEMetricSpace.edist_self, Unique.eq_default, LT.lt.ne', one_div, add_zero, WithLp.prod_edist_eq_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : Unique β
⊢ Eq (α := (a : WithLp p (α × β)) → α) (⇑(withLpProdUnique p α β) : (a : WithLp p (α × β)) → α) WithLp.fst

Tactic:
rfl

Premises used: WithLp.fst, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : Unique α
⊢ Eq (α := (a : WithLp p (α × β)) → β) (⇑(withLpUniqueProd p α β) : (a : WithLp p (α × β)) → β) WithLp.snd

Tactic:
rfl

Premises used: WithLp.snd, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup α
inst_2 : Module 𝕜 α
inst_3 : SeminormedAddCommGroup β
inst_4 : Module 𝕜 β
x : WithLp p (α × β)
⊢ (withLpProdComm p 𝕜 α β : (a : WithLp p (α × β)) → WithLp p (β × α)) x = WithLp.toLp p (x.snd, x.fst)

Tactic:
rfl

Premises used: WithLp.snd, WithLp.fst, Prod.swap, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup α
inst_2 : Module 𝕜 α
inst_3 : SeminormedAddCommGroup β
inst_4 : Module 𝕜 β
⊢ Eq (α := WithLp p (β × α) ≃ₗᵢ[𝕜] WithLp p (α × β)) (symm (withLpProdComm p 𝕜 α β)) (withLpProdComm p 𝕜 β α)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, LinearIsometryEquiv.withLpProdComm, LinearEquiv.withLpCongr, Prod.swap, LinearEquiv.trans, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup α
inst_2 : Module 𝕜 α
inst_3 : SeminormedAddCommGroup β
inst_4 : Module 𝕜 β
inst_5 : Unique β
⊢ Eq (α := (a : WithLp p (α × β)) → α) (⇑(withLpProdUnique p 𝕜 α β) : (a : WithLp p (α × β)) → α) WithLp.fst

Tactic:
rfl

Premises used: WithLp.fst, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup α
inst_2 : Module 𝕜 α
inst_3 : SeminormedAddCommGroup β
inst_4 : Module 𝕜 β
inst_5 : Unique α
⊢ Eq (α := (a : WithLp p (α × β)) → β) (⇑(withLpUniqueProd p 𝕜 α β) : (a : WithLp p (α × β)) → β) WithLp.snd

Tactic:
rfl

Premises used: WithLp.snd, rfl
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
inl : ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε
inr : ∀ (hp : p ≠ ∞), ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
rcases eq_or_ne p ∞ with rfl | hp

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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 μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
⊢ Continuous (Y := ℝ) fun (x : E) ↦ ε

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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 μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
x : E
⊢ LT.lt (α := ℝ) 0 ((fun (x : E) ↦ ε) x)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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 μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
inl :
  ∀ (g : E → F) (hg₁ : ContDiff ℝ ∞ g) (hg₂ : ∀ (x : E), dist (g x) (f x) < ε)
    (hg₃ : Function.support g ⊆ Function.support f),
    ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨g, hg₁, hg₂, hg₃⟩ := h₂.exists_contDiff_approx ⊤ (ε := fun _ ↦ ε) (by fun_prop)
      (by intro; positivity)

Premises used: Continuous.exists_contDiff_approx, Top.top
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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 μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε
hg₃ : Function.support g ⊆ Function.support f
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε

Tactic:
⟨g, h₁.mono hg₃, hg₁, eLpNormEssSup_le_of_ae_bound (.of_forall fun x ↦ ?_)⟩

Premises used: Filter.Eventually.of_forall, MeasureTheory.eLpNormEssSup_le_of_ae_bound, HasCompactSupport.mono, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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 μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε
hg₃ : Function.support g ⊆ Function.support f
inl : ∀ (x : E), ‖(f - g) x‖ ≤ ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨g, h₁.mono hg₃, hg₁, eLpNormEssSup_le_of_ae_bound (.of_forall fun x ↦ ?_)⟩
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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 μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε
hg₃ : Function.support g ⊆ Function.support f
x : E
⊢ ‖(f - g) x‖ ≤ ε

Tactic:
simpa [← dist_eq_norm_sub'] using (hg₂ x).le

Premises used: LT.lt.le, dist_eq_norm_sub'
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
pos :
  ∀ (hf : f =ᶠ[ae μ] 0), ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
neg :
  ∀ (hf : ¬f =ᶠ[ae μ] 0), ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
by_cases hf : f =ᵐ[μ] 0
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : f =ᶠ[ae μ] 0
h :
  HasCompactSupport.{u_3, u_4} (α := E) (β := F) 0 ∧
    ContDiff.{0, u_3, u_4} ℝ (E := E) (F := F) ∞ 0 ∧ eLpNorm (f - 0) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
use 0
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : f =ᶠ[ae μ] 0
⊢ HasCompactSupport.{u_3, u_4} (α := E) (β := F) 0 ∧
    ContDiff.{0, u_3, u_4} ℝ (E := E) (F := F) ∞ 0 ∧ eLpNorm (f - 0) p μ ≤ ENNReal.ofReal ε

Tactic:
simpa [HasCompactSupport.zero, eLpNorm_congr_ae hf] using contDiff_const

Premises used: contDiff_const, HasCompactSupport.zero, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hs₁ : μ (tsupport f) ≠ ⊤ := h₁.measure_lt_top.ne
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← Measure.measure_support_eq_zero_iff _] at hf

Premises used: MeasureTheory.Measure.measure_support_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hf₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← Measure.measure_support_eq_zero_iff _] at hf

Premises used: MeasureTheory.Measure.measure_support_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))

Tactic:
toReal_pos (pos_mono (subset_tsupport f) (pos_of_ne_zero hf)).ne' hs₁

Premises used: subset_tsupport, ENNReal.toReal_pos, LT.lt.ne', MeasureTheory.pos_mono, pos_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))

Tactic:
exact toReal_pos (pos_mono (subset_tsupport f) (pos_of_ne_zero hf)).ne' hs₁

Premises used: subset_tsupport, ENNReal.toReal_pos, LT.lt.ne', MeasureTheory.pos_mono, pos_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))

Tactic:
have hs₂ : 0 < (μ <| tsupport f).toReal := by
    -- Since `f` is not the zero function `tsupport f` has positive measure
    rw [← Measure.measure_support_eq_zero_iff _] at hf
    exact toReal_pos (pos_mono (subset_tsupport f) (pos_of_ne_zero hf)).ne' hs₁
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
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∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
⊢ let ε' := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal));
  ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))

Tactic:
set ε' := ε * (μ <| tsupport f).toReal ^ (-(1 / p.toReal)) with ε'_def

Premises used: HDiv.hDiv, tsupport, ENNReal.toReal, OfNat.ofNat, DFunLike.coe, Neg.neg