awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ ∫ (x : E) in closedBall c f.rOut, 1 ∂μ = μ.real (closedBall c f.rOut)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
f₁ : Eq (α := ℝ) (∫ (x : E), (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ)
f₂ : LE.le (α := ℝ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, 1 ∂μ)
f₃ : ∫ (x : E) in closedBall c f.rOut, 1 ∂μ = μ.real (closedBall c f.rOut)
⊢ ∫ (x : E), (↑f : E → ℝ) x ∂μ ≤ μ.real (closedBall c f.rOut)

Tactic:
calc
  ∫ x, f x ∂μ = ∫ x in closedBall c f.rOut, f x ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    apply f.zero_of_le_dist (le_of_lt _)
    simpa using hx
  _ ≤ ∫ x in closedBall c f.rOut, 1 ∂μ := by
    apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
    simp [measure_closedBall_lt_top]
  _ = μ.real (closedBall c f.rOut) := by simp

Premises used: MeasureTheory.Measure.real, ContDiffBump.rOut, Metric.closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
⊢ 0 < K

Tactic:
simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)

Premises used: Iff.mpr, LT.lt.le, mul_pos_iff, not_lt, LT.lt.trans_le, Iff.mp, ContDiffBump.rIn_pos, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
⊢ 0 < K

Tactic:
have K_pos : 0 < K := by
    simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
apply : μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ μ.real (closedBall c f.rIn)
⊢ μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ

Tactic:
apply le_trans _ (f.measure_closedBall_le_integral μ)

Premises used: ContDiffBump.measure_closedBall_le_integral, le_trans
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
rw : f.rOut ^ finrank ℝ E * μ.real (closedBall 0 1) ≤ (K * f.rIn) ^ finrank ℝ E * μ.real (closedBall 0 1)
⊢ μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ μ.real (closedBall c f.rIn)

Tactic:
rw [div_le_iff₀ (pow_pos K_pos _), addHaar_real_closedBall' _ _ f.rIn_pos.le,
    addHaar_real_closedBall' _ _ f.rOut_pos.le, mul_assoc, mul_comm _ (K ^ _), ← mul_assoc,
    ← mul_pow, mul_comm _ K]

Premises used: div_le_iff₀, pow_pos, mul_assoc, LT.lt.le, MeasureTheory.Measure.addHaar_real_closedBall', HPow.hPow, mul_comm, mul_pow, ContDiffBump.rIn_pos, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
hbc : 0 ≤ f.rOut
⊢ f.rOut ^ finrank ℝ E * μ.real (closedBall 0 1) ≤ (K * f.rIn) ^ finrank ℝ E * μ.real (closedBall 0 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ 0 ≤ f.rOut

Tactic:
f.rOut_pos.le

Premises used: LT.lt.le, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ 0 ≤ f.rOut

Tactic:
exact f.rOut_pos.le

Premises used: LT.lt.le, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
⊢ 0 < K

Tactic:
simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)

Premises used: Iff.mpr, LT.lt.le, mul_pos_iff, not_lt, LT.lt.trans_le, Iff.mp, ContDiffBump.rIn_pos, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
⊢ 0 < K

Tactic:
have K_pos : 0 < K := by
    simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
hc : LE.le (α := ℝ) 0 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
hab : (↑f : E → ℝ) x ≤ 1
⊢ (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ LE.le (α := ℝ) 0 (∫ (y : E), (↑f : E → ℝ) y ∂μ)

Tactic:
f.integral_pos.le

Premises used: LT.lt.le, ContDiffBump.integral_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ LE.le (α := ℝ) 0 (∫ (y : E), (↑f : E → ℝ) y ∂μ)

Tactic:
exact f.integral_pos.le

Premises used: LT.lt.le, ContDiffBump.integral_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ (↑f : E → ℝ) x ≤ 1

Tactic:
f.le_one

Premises used: ContDiffBump.le_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ (↑f : E → ℝ) x ≤ 1

Tactic:
exact f.le_one

Premises used: ContDiffBump.le_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)

Tactic:
have : f x / ∫ y, f y ∂μ ≤ 1 / ∫ y, f y ∂μ := by
    gcongr
    · exact f.integral_pos.le
    · exact f.le_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
apply : HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ) ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut)
⊢ f.normed μ x ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut)

Tactic:
apply this.trans

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
rw : μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ
rw₁ : 0 < μ.real (closedBall c f.rOut)
⊢ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ) ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut)

Tactic:
rw [div_le_div_iff₀ f.integral_pos, one_mul, ← div_le_iff₀' (pow_pos K_pos _)]

Premises used: pow_pos, div_le_div_iff₀, div_le_iff₀', one_mul, ContDiffBump.integral_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
⊢ μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ

Tactic:
f.measure_closedBall_div_le_integral μ K h

Premises used: ContDiffBump.measure_closedBall_div_le_integral
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
⊢ μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ

Tactic:
exact f.measure_closedBall_div_le_integral μ K h

Premises used: ContDiffBump.measure_closedBall_div_le_integral
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
⊢ 0 < μ.real (closedBall c f.rOut)

Tactic:
ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rOut_pos).ne'
      measure_closedBall_lt_top.ne

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_pos, LT.lt.ne', Metric.measure_closedBall_pos, MeasureTheory.measure_closedBall_lt_top, LT.lt.ne, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
⊢ 0 < μ.real (closedBall c f.rOut)

Tactic:
exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rOut_pos).ne'
      measure_closedBall_lt_top.ne

Premises used: ENNReal.toReal_pos, LT.lt.ne', Metric.measure_closedBall_pos, MeasureTheory.measure_closedBall_lt_top, LT.lt.ne, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
hf : LocallyIntegrable f μ
hε : 0 < ε
φ : ContDiffBump.{u_1} (E := E) 0 := { rIn := ε / 2, rOut := ε, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ

Tactic:
⟨_, ?_, fun a δ ↦ φ.dist_normed_convolution_le hf.aestronglyMeasurable⟩

Premises used: And.intro, ContDiffBump.dist_normed_convolution_le, Exists.intro, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
hf : LocallyIntegrable f μ
hε : 0 < ε
φ : ContDiffBump.{u_1} (E := E) 0 := { rIn := ε / 2, rOut := ε, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
refine :
  ContDiff.{0, u_1, u_2} ℝ (F := F) ∞ fun (a : E) ↦ convolution (φ.normed μ) f (ContinuousLinearMap.lsmul ℝ ℝ) μ a
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ

Tactic:
refine ⟨_, ?_, fun a δ ↦ φ.dist_normed_convolution_le hf.aestronglyMeasurable⟩
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
hf : LocallyIntegrable f μ
hε : 0 < ε
φ : ContDiffBump.{u_1} (E := E) 0 := { rIn := ε / 2, rOut := ε, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
⊢ ContDiff.{0, u_1, u_2} ℝ (F := F) ∞ fun (a : E) ↦ convolution (φ.normed μ) f (ContinuousLinearMap.lsmul ℝ ℝ) μ a

Tactic:
φ.hasCompactSupport_normed.contDiff_convolution_left _ φ.contDiff_normed hf

Premises used: ContDiffBump.contDiff_normed, HasCompactSupport.contDiff_convolution_left, ContDiffBump.hasCompactSupport_normed
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
hf : LocallyIntegrable f μ
hε : 0 < ε
φ : ContDiffBump.{u_1} (E := E) 0 := { rIn := ε / 2, rOut := ε, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
⊢ ContDiff.{0, u_1, u_2} ℝ (F := F) ∞ fun (a : E) ↦ convolution (φ.normed μ) f (ContinuousLinearMap.lsmul ℝ ℝ) μ a

Tactic:
exact φ.hasCompactSupport_normed.contDiff_convolution_left _ φ.contDiff_normed hf

Premises used: ContDiffBump.contDiff_normed, HasCompactSupport.contDiff_convolution_left, ContDiffBump.hasCompactSupport_normed
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hε : 0 < ε
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hε : 0 < ε
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ

Tactic:
(hf.locallyIntegrable (μ := .addHaar)).exists_contDiff_dist_le_of_forall_mem_ball_dist_le hε

Premises used: MeasureTheory.LocallyIntegrable.exists_contDiff_dist_le_of_forall_mem_ball_dist_le, Continuous.locallyIntegrable
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hε : 0 < ε
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ

Tactic:
exact (hf.locallyIntegrable (μ := .addHaar)).exists_contDiff_dist_le_of_forall_mem_ball_dist_le hε

Premises used: MeasureTheory.LocallyIntegrable.exists_contDiff_dist_le_of_forall_mem_ball_dist_le, Continuous.locallyIntegrable
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
hf : UniformContinuous f
hε : 0 < ε
rcases :
  ∀ (δ : ℝ) (hδ : δ > 0) (hfδ : ∀ ⦃a b : E⦄, dist a b < δ → dist (f a) (f b) < ε / 2),
    ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E), dist (g a) (f a) < ε
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E), dist (g a) (f a) < ε

Tactic:
rcases Metric.uniformContinuous_iff.mp hf (ε / 2) (half_pos hε) with ⟨δ, hδ, hfδ⟩

Premises used: half_pos, HDiv.hDiv, Iff.mp, OfNat.ofNat, Metric.uniformContinuous_iff
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
hf : UniformContinuous f
hε : 0 < ε
δ : ℝ
hδ : δ > 0
hfδ : ∀ ⦃a b : E⦄, dist a b < δ → dist (f a) (f b) < ε / 2
rcases :
  ∀ (g : E → F) (hgc : ContDiff ℝ ∞ g)
    (hg : ∀ (a : E) (δ_1 : ℝ), (∀ x ∈ ball a δ, dist (f x) (f a) ≤ δ_1) → dist (g a) (f a) ≤ δ_1),
    ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E), dist (g a) (f a) < ε
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E), dist (g a) (f a) < ε

Tactic:
rcases hf.continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le hδ with ⟨g, hgc, hg⟩

Premises used: Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le, UniformContinuous.continuous
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
hf : UniformContinuous f
hε : 0 < ε
δ : ℝ
hδ : δ > 0
hfδ : ∀ ⦃a b : E⦄, dist a b < δ → dist (f a) (f b) < ε / 2
g : E → F
hgc : ContDiff ℝ ∞ g
hg : ∀ (a : E) (δ_1 : ℝ), (∀ x ∈ ball a δ, dist (f x) (f a) ≤ δ_1) → dist (g a) (f a) ≤ δ_1
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E), dist (g a) (f a) < ε

Tactic:
⟨g, hgc, fun a ↦ (hg a _ fun _ h ↦ (hfδ h).le).trans_lt (half_lt_self hε)⟩

Premises used: half_lt_self, HDiv.hDiv, LT.lt.le, And.intro, Exists.intro, OfNat.ofNat, LE.le.trans_lt
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
ε : ℝ
hf : UniformContinuous f
hε : 0 < ε
δ : ℝ
hδ : δ > 0
hfδ : ∀ ⦃a b : E⦄, dist a b < δ → dist (f a) (f b) < ε / 2
g : E → F
hgc : ContDiff ℝ ∞ g
hg : ∀ (a : E) (δ_1 : ℝ), (∀ x ∈ ball a δ, dist (f x) (f a) ≤ δ_1) → dist (g a) (f a) ≤ δ_1
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E), dist (g a) (f a) < ε

Tactic:
exact ⟨g, hgc, fun a ↦ (hg a _ fun _ h ↦ (hfδ h).le).trans_lt (half_lt_self hε)⟩
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
rw :
  ∀ (i : Set E × ℝ),
    IsCompact i.1 ∧ 0 < i.2 →
      ∃ (y : C(E, F)),
        Membership.mem (γ := Set C(E, F))
            {f : C(E, F) | ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑f : (a : E) → F)} y ∧
          Membership.mem (γ := Set C(E, F))
            {y : C(E, F) |
              Membership.mem (γ := SetRel C(E, F) C(E, F))
                {fg : C(E, F) × C(E, F) |
                  ∀ x ∈ i.1,
                    Membership.mem.{u_2, u_2} (α := F × F) (γ := Set (F × F)) {p : F × F | dist p.1 p.2 < i.2}
                      (((fg.1 : (a : E) → F) x, (fg.2 : (a : E) → F) x) : F × F)}
                (y, f)}
            y
⊢ Membership.mem (γ := Set C(E, F))
    (closure {f : C(E, F) | ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑f : (a : E) → F)}) f

Tactic:
rw [mem_closure_iff_nhds_basis
    (nhds_basis_uniformity uniformity_basis_dist.compactConvergenceUniformity)]

Premises used: Metric.uniformity_basis_dist, Filter.HasBasis.compactConvergenceUniformity, nhds_basis_uniformity, mem_closure_iff_nhds_basis