diff --git a/docs/overview.yaml b/docs/overview.yaml
index 4c85da0604c81..1857a175084bf 100644
--- a/docs/overview.yaml
+++ b/docs/overview.yaml
@@ -337,7 +337,7 @@ Analysis:
     Fubini's theorem: 'measure_theory.integral_prod'
     product of finitely many measures: 'measure_theory.measure.pi'
     convolution: 'convolution'
-    approximation by convolution: 'cont_diff_bump_of_inner.convolution_tendsto_right'
+    approximation by convolution: 'cont_diff_bump.convolution_tendsto_right'
     regularization by convolution: 'has_compact_support.cont_diff_convolution_left'
     change of variables formula: 'measure_theory.integral_image_eq_integral_abs_det_fderiv_smul'
     divergence theorem: 'measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable'
diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
index 18d92c12e930f..c984b13916c83 100644
--- a/docs/undergrad.yaml
+++ b/docs/undergrad.yaml
@@ -518,7 +518,7 @@ Measures and integral calculus:
     change of variables to polar co-ordinates: 'integral_comp_polar_coord_symm '
     change of variables to spherical co-ordinates: ''
     convolution: 'convolution'
-    approximation by convolution: 'cont_diff_bump_of_inner.convolution_tendsto_right'
+    approximation by convolution: 'cont_diff_bump.convolution_tendsto_right'
     regularization by convolution: 'has_compact_support.cont_diff_convolution_left'
   Fourier analysis:
     Fourier series of locally integrable periodic real-valued functions: 'fourier_basis'
diff --git a/src/analysis/calculus/bump_function_findim.lean b/src/analysis/calculus/bump_function_findim.lean
index 0ea049edb8028..848daeca1936b 100644
--- a/src/analysis/calculus/bump_function_findim.lean
+++ b/src/analysis/calculus/bump_function_findim.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import analysis.calculus.specific_functions
+import analysis.calculus.bump_function_inner
 import analysis.calculus.series
 import analysis.convolution
 import data.set.pointwise.support
@@ -16,9 +16,8 @@ Let `E` be a finite-dimensional real normed vector space. We show that any open
 exactly the support of a smooth function taking values in `[0, 1]`,
 in `is_open.exists_smooth_support_eq`.
 
-TODO: use this construction to construct bump functions with nice behavior in any finite-dimensional
-real normed vector space, by convolving the indicator function of `closed_ball 0 1` with a
-function as above with `s = ball 0 D`.
+Then we use this construction to construct bump functions with nice behavior, by convolving
+the indicator function of `closed_ball 0 1` with a function as above with `s = ball 0 D`.
 -/
 
 noncomputable theory
@@ -41,7 +40,7 @@ theorem exists_smooth_tsupport_subset {s : set E} {x : E} (hs : s ∈ 𝓝 x) :
 begin
   obtain ⟨d, d_pos, hd⟩ : ∃ (d : ℝ) (hr : 0 < d), euclidean.closed_ball x d ⊆ s,
     from euclidean.nhds_basis_closed_ball.mem_iff.1 hs,
-  let c : cont_diff_bump_of_inner (to_euclidean x) :=
+  let c : cont_diff_bump (to_euclidean x) :=
   { r := d/2,
     R := d,
     r_pos := half_pos d_pos,
@@ -478,25 +477,6 @@ variable {E}
 
 end helper_definitions
 
-/-- The base function from which one will construct a family of bump functions. One could
-add more properties if they are useful and satisfied in the examples of inner product spaces
-and finite dimensional vector spaces, notably derivative norm control in terms of `R - 1`.
-TODO: move to the right file and use this to refactor bump functions in general. -/
-@[nolint has_nonempty_instance]
-structure _root_.cont_diff_bump_base (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] :=
-(to_fun : ℝ → E → ℝ)
-(mem_Icc   : ∀ (R : ℝ) (x : E), to_fun R x ∈ Icc (0 : ℝ) 1)
-(symmetric : ∀ (R : ℝ) (x : E), to_fun R (-x) = to_fun R x)
-(smooth    : cont_diff_on ℝ ⊤ (uncurry to_fun) ((Ioi (1 : ℝ)) ×ˢ (univ : set E)))
-(eq_one    : ∀ (R : ℝ) (hR : 1 < R) (x : E) (hx : ‖x‖ ≤ 1), to_fun R x = 1)
-(support   : ∀ (R : ℝ) (hR : 1 < R), support (to_fun R) = metric.ball (0 : E) R)
-
-/-- A class registering that a real vector space admits bump functions. This will be instantiated
-first for inner product spaces, and then for finite-dimensional normed spaces.
-We use a specific class instead of `nonempty (cont_diff_bump_base E)` for performance reasons. -/
-class _root_.has_cont_diff_bump (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] : Prop :=
-(out : nonempty (cont_diff_bump_base E))
-
 @[priority 100]
 instance {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :
   has_cont_diff_bump E :=
diff --git a/src/analysis/calculus/specific_functions.lean b/src/analysis/calculus/bump_function_inner.lean
similarity index 67%
rename from src/analysis/calculus/specific_functions.lean
rename to src/analysis/calculus/bump_function_inner.lean
index 7cca302310603..8a8987b7af8cd 100644
--- a/src/analysis/calculus/specific_functions.lean
+++ b/src/analysis/calculus/bump_function_inner.lean
@@ -20,29 +20,19 @@ function cannot have:
 * `real.smooth_transition` is equal to zero for `x ≤ 0` and is equal to one for `x ≥ 1`; it is given
   by `exp_neg_inv_glue x / (exp_neg_inv_glue x + exp_neg_inv_glue (1 - x))`;
 
-* `f : cont_diff_bump_of_inner c`, where `c` is a point in an inner product space, is
+* `f : cont_diff_bump c`, where `c` is a point in a real vector space, is
   a bundled smooth function such that
 
   - `f` is equal to `1` in `metric.closed_ball c f.r`;
   - `support f = metric.ball c f.R`;
   - `0 ≤ f x ≤ 1` for all `x`.
 
-  The structure `cont_diff_bump_of_inner` contains the data required to construct the
+  The structure `cont_diff_bump` contains the data required to construct the
   function: real numbers `r`, `R`, and proofs of `0 < r < R`. The function itself is available
   through `coe_fn`.
 
-* If `f : cont_diff_bump_of_inner c` and `μ` is a measure on the domain of `f`, then `f.normed μ`
+* If `f : cont_diff_bump c` and `μ` is a measure on the domain of `f`, then `f.normed μ`
   is a smooth bump function with integral `1` w.r.t. `μ`.
-
-* `f : cont_diff_bump c`, where `c` is a point in a finite dimensional real vector space, is a
-  bundled smooth function such that
-
-  - `f` is equal to `1` in `euclidean.closed_ball c f.r`;
-  - `support f = euclidean.ball c f.R`;
-  - `0 ≤ f x ≤ 1` for all `x`.
-
-  The structure `cont_diff_bump` contains the data required to construct the function: real
-  numbers `r`, `R`, and proofs of `0 < r < R`. The function itself is available through `coe_fn`.
 -/
 
 noncomputable theory
@@ -275,76 +265,173 @@ end real
 
 variables {E X : Type*}
 
-/-- `f : cont_diff_bump_of_inner c`, where `c` is a point in an inner product space, is a
+/-- `f : cont_diff_bump c`, where `c` is a point in a normed vector space, is a
 bundled smooth function such that
 
 - `f` is equal to `1` in `metric.closed_ball c f.r`;
 - `support f = metric.ball c f.R`;
 - `0 ≤ f x ≤ 1` for all `x`.
 
-The structure `cont_diff_bump_of_inner` contains the data required to construct the function:
+The structure `cont_diff_bump` contains the data required to construct the function:
 real numbers `r`, `R`, and proofs of `0 < r < R`. The function itself is available through
-`coe_fn`. -/
-structure cont_diff_bump_of_inner (c : E) :=
+`coe_fn` when the space is nice enough, i.e., satisfies the `has_cont_diff_bump` typeclass. -/
+structure cont_diff_bump (c : E) :=
 (r R : ℝ)
 (r_pos : 0 < r)
 (r_lt_R : r < R)
 
-namespace cont_diff_bump_of_inner
+/-- The base function from which one will construct a family of bump functions. One could
+add more properties if they are useful and satisfied in the examples of inner product spaces
+and finite dimensional vector spaces, notably derivative norm control in terms of `R - 1`. -/
+@[nolint has_nonempty_instance]
+structure cont_diff_bump_base (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] :=
+(to_fun : ℝ → E → ℝ)
+(mem_Icc   : ∀ (R : ℝ) (x : E), to_fun R x ∈ Icc (0 : ℝ) 1)
+(symmetric : ∀ (R : ℝ) (x : E), to_fun R (-x) = to_fun R x)
+(smooth    : cont_diff_on ℝ ⊤ (uncurry to_fun) ((Ioi (1 : ℝ)) ×ˢ (univ : set E)))
+(eq_one    : ∀ (R : ℝ) (hR : 1 < R) (x : E) (hx : ‖x‖ ≤ 1), to_fun R x = 1)
+(support   : ∀ (R : ℝ) (hR : 1 < R), support (to_fun R) = metric.ball (0 : E) R)
+
+/-- A class registering that a real vector space admits bump functions. This will be instantiated
+first for inner product spaces, and then for finite-dimensional normed spaces.
+We use a specific class instead of `nonempty (cont_diff_bump_base E)` for performance reasons. -/
+class has_cont_diff_bump (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] : Prop :=
+(out : nonempty (cont_diff_bump_base E))
+
+/-- In a space with `C^∞` bump functions, register some function that will be used as a basis
+to construct bump functions of arbitrary size around any point. -/
+def some_cont_diff_bump_base (E : Type*) [normed_add_comm_group E] [normed_space ℝ E]
+  [hb : has_cont_diff_bump E] : cont_diff_bump_base E :=
+nonempty.some hb.out
+
+/-- Any inner product space has smooth bump functions. -/
+@[priority 100] instance has_cont_diff_bump_of_inner_product_space
+  (E : Type*) [inner_product_space ℝ E] : has_cont_diff_bump E :=
+let e : cont_diff_bump_base E :=
+{ to_fun := λ R x, real.smooth_transition ((R - ‖x‖) / (R - 1)),
+  mem_Icc := λ R x, ⟨real.smooth_transition.nonneg _, real.smooth_transition.le_one _⟩,
+  symmetric := λ R x, by simp only [norm_neg],
+  smooth := begin
+    rintros ⟨R, x⟩ ⟨(hR : 1 < R), hx⟩,
+    apply cont_diff_at.cont_diff_within_at,
+    rcases eq_or_ne x 0 with rfl|hx,
+    { have : (λ (p : ℝ × E), real.smooth_transition ((p.1 - ‖p.2‖) / (p.1 - 1)))
+        =ᶠ[𝓝 (R, 0)] (λ p, 1),
+      { have A : tendsto (λ (p : ℝ × E), (p.1 - ‖p.2‖) / (p.1 - 1))
+          (𝓝 (R, 0)) (𝓝 ((R - ‖(0 : E)‖) / (R - 1))),
+        { rw nhds_prod_eq,
+          apply (tendsto_fst.sub tendsto_snd.norm).div (tendsto_fst.sub tendsto_const_nhds),
+          exact (sub_pos.2 hR).ne' },
+        have : ∀ᶠ (p : ℝ × E) in 𝓝 (R, 0), 1 < (p.1 - ‖p.2‖) / (p.1 - 1),
+        { apply (tendsto_order.1 A).1,
+          apply (one_lt_div (sub_pos.2 hR)).2,
+          simp only [norm_zero, tsub_zero, sub_lt_self_iff, zero_lt_one] },
+        filter_upwards [this] with q hq,
+        exact real.smooth_transition.one_of_one_le hq.le },
+      exact cont_diff_at_const.congr_of_eventually_eq this },
+    { refine real.smooth_transition.cont_diff_at.comp _ _,
+      refine cont_diff_at.div _ _ (sub_pos.2 hR).ne',
+      { exact cont_diff_at_fst.sub (cont_diff_at_snd.norm hx) },
+      { exact cont_diff_at_fst.sub cont_diff_at_const } }
+  end,
+  eq_one := λ R hR x hx, real.smooth_transition.one_of_one_le $
+    (one_le_div (sub_pos.2 hR)).2 (sub_le_sub_left hx _),
+  support := λ R hR, begin
+    apply subset.antisymm,
+    { assume x hx,
+      simp only [mem_support] at hx,
+      contrapose! hx,
+      simp only [mem_ball_zero_iff, not_lt] at hx,
+      apply real.smooth_transition.zero_of_nonpos,
+      apply div_nonpos_of_nonpos_of_nonneg;
+      linarith },
+    { assume x hx,
+      simp only [mem_ball_zero_iff] at hx,
+      apply (real.smooth_transition.pos_of_pos _).ne',
+      apply div_pos;
+      linarith }
+  end, }
+in ⟨⟨e⟩⟩
+
+namespace cont_diff_bump
+
+lemma R_pos {c : E} (f : cont_diff_bump c) : 0 < f.R := f.r_pos.trans f.r_lt_R
 
-lemma R_pos {c : E} (f : cont_diff_bump_of_inner c) : 0 < f.R := f.r_pos.trans f.r_lt_R
+lemma one_lt_R_div_r {c : E} (f : cont_diff_bump c) : 1 < f.R / f.r :=
+begin
+  rw one_lt_div f.r_pos,
+  exact f.r_lt_R
+end
 
-instance (c : E) : inhabited (cont_diff_bump_of_inner c) := ⟨⟨1, 2, zero_lt_one, one_lt_two⟩⟩
+instance (c : E) : inhabited (cont_diff_bump c) := ⟨⟨1, 2, zero_lt_one, one_lt_two⟩⟩
 
-variables [inner_product_space ℝ E] [normed_add_comm_group X] [normed_space ℝ X]
-variables {c : E} (f : cont_diff_bump_of_inner c) {x : E} {n : ℕ∞}
+variables [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group X] [normed_space ℝ X]
+[has_cont_diff_bump E] {c : E} (f : cont_diff_bump c) {x : E} {n : ℕ∞}
 
-/-- The function defined by `f : cont_diff_bump_of_inner c`. Use automatic coercion to
+/-- The function defined by `f : cont_diff_bump c`. Use automatic coercion to
 function instead. -/
-def to_fun (f : cont_diff_bump_of_inner c) : E → ℝ :=
-λ x, real.smooth_transition ((f.R - dist x c) / (f.R - f.r))
+def to_fun {c : E} (f : cont_diff_bump c) : E → ℝ :=
+λ x, (some_cont_diff_bump_base E).to_fun (f.R / f.r) (f.r⁻¹ • (x - c))
 
-instance : has_coe_to_fun (cont_diff_bump_of_inner c) (λ _, E → ℝ) := ⟨to_fun⟩
+instance : has_coe_to_fun (cont_diff_bump c) (λ _, E → ℝ) := ⟨to_fun⟩
 
-protected lemma «def» (x : E) : f x = real.smooth_transition ((f.R - dist x c) / (f.R - f.r)) :=
+protected lemma «def» (x : E) :
+  f x = (some_cont_diff_bump_base E).to_fun (f.R / f.r) (f.r⁻¹ • (x - c)) :=
 rfl
 
 protected lemma sub (x : E) : f (c - x) = f (c + x) :=
-by simp_rw [f.def, dist_self_sub_left, dist_self_add_left]
+by simp [f.def, cont_diff_bump_base.symmetric]
 
-protected lemma neg (f : cont_diff_bump_of_inner (0 : E)) (x : E) : f (- x) = f x :=
+protected lemma neg (f : cont_diff_bump (0 : E)) (x : E) : f (- x) = f x :=
 by simp_rw [← zero_sub, f.sub, zero_add]
 
-open real (smooth_transition) real.smooth_transition metric
+open metric
 
 lemma one_of_mem_closed_ball (hx : x ∈ closed_ball c f.r) :
   f x = 1 :=
-one_of_one_le $ (one_le_div (sub_pos.2 f.r_lt_R)).2 $ sub_le_sub_left hx _
+begin
+  apply cont_diff_bump_base.eq_one _ _ f.one_lt_R_div_r,
+  simpa only [norm_smul, norm_eq_abs, abs_inv, abs_of_nonneg f.r_pos.le, ← div_eq_inv_mul,
+    div_le_one f.r_pos] using mem_closed_ball_iff_norm.1 hx
+end
 
-lemma nonneg : 0 ≤ f x := nonneg _
+lemma nonneg : 0 ≤ f x :=
+(cont_diff_bump_base.mem_Icc ((some_cont_diff_bump_base E)) _ _).1
 
-/-- A version of `cont_diff_bump_of_inner.nonneg` with `x` explicit -/
+/-- A version of `cont_diff_bump.nonneg` with `x` explicit -/
 lemma nonneg' (x : E) : 0 ≤ f x :=
 f.nonneg
 
-lemma le_one : f x ≤ 1 := le_one _
+lemma le_one : f x ≤ 1 :=
+(cont_diff_bump_base.mem_Icc ((some_cont_diff_bump_base E)) _ _).2
 
 lemma pos_of_mem_ball (hx : x ∈ ball c f.R) : 0 < f x :=
-pos_of_pos $ div_pos (sub_pos.2 hx) (sub_pos.2 f.r_lt_R)
-
-lemma lt_one_of_lt_dist (h : f.r < dist x c) : f x < 1 :=
-lt_one_of_lt_one $ (div_lt_one (sub_pos.2 f.r_lt_R)).2 $ sub_lt_sub_left h _
+begin
+  refine lt_iff_le_and_ne.2 ⟨f.nonneg, ne.symm _⟩,
+  change (f.r)⁻¹ • (x - c) ∈ support ((some_cont_diff_bump_base E).to_fun (f.R / f.r)),
+  rw cont_diff_bump_base.support _ _ f.one_lt_R_div_r,
+  simp only [dist_eq_norm, mem_ball] at hx,
+  simpa only [norm_smul, mem_ball_zero_iff, norm_eq_abs, abs_inv, abs_of_nonneg f.r_pos.le,
+    ← div_eq_inv_mul] using (div_lt_div_right f.r_pos).2 hx,
+end
 
 lemma zero_of_le_dist (hx : f.R ≤ dist x c) : f x = 0 :=
-zero_of_nonpos $ div_nonpos_of_nonpos_of_nonneg (sub_nonpos.2 hx) (sub_nonneg.2 f.r_lt_R.le)
+begin
+  rw dist_eq_norm at hx,
+  suffices H : (f.r)⁻¹ • (x - c) ∉ support ((some_cont_diff_bump_base E).to_fun (f.R / f.r)),
+    by simpa only [mem_support, not_not] using H,
+  rw cont_diff_bump_base.support _ _ f.one_lt_R_div_r,
+  simp [norm_smul, norm_eq_abs, abs_inv, abs_of_nonneg f.r_pos.le, ← div_eq_inv_mul],
+  exact div_le_div_of_le f.r_pos.le hx,
+end
 
 lemma support_eq : support (f : E → ℝ) = metric.ball c f.R :=
 begin
   ext x,
   suffices : f x ≠ 0 ↔ dist x c < f.R, by simpa [mem_support],
   cases lt_or_le (dist x c) f.R with hx hx,
-  { simp [hx, (f.pos_of_mem_ball hx).ne'] },
-  { simp [hx.not_lt, f.zero_of_le_dist hx] }
+  { simp only [hx, (f.pos_of_mem_ball hx).ne', ne.def, not_false_iff]},
+  { simp only [hx.not_lt, f.zero_of_le_dist hx, ne.def, eq_self_iff_true, not_true] }
 end
 
 lemma tsupport_eq : tsupport f = closed_ball c f.R :=
@@ -363,7 +450,7 @@ f.eventually_eq_one_of_mem_ball (mem_ball_self f.r_pos)
 
 /-- `cont_diff_bump` is `𝒞ⁿ` in all its arguments. -/
 protected lemma _root_.cont_diff_at.cont_diff_bump {c g : X → E}
-  {f : ∀ x, cont_diff_bump_of_inner (c x)} {x : X}
+  {f : ∀ x, cont_diff_bump (c x)} {x : X}
   (hc : cont_diff_at ℝ n c x) (hr : cont_diff_at ℝ n (λ x, (f x).r) x)
   (hR : cont_diff_at ℝ n (λ x, (f x).R) x)
   (hg : cont_diff_at ℝ n g x) : cont_diff_at ℝ n (λ x, f x (g x)) x :=
@@ -376,11 +463,18 @@ begin
       exact eventually_of_mem this
         (λ x hx, (f x).one_of_mem_closed_ball (mem_set_of_eq.mp hx).le) },
     exact cont_diff_at_const.congr_of_eventually_eq this },
-  { refine real.smooth_transition.cont_diff_at.comp x _,
-    refine ((hR.sub $ hg.dist hc hx).div (hR.sub hr) (sub_pos.mpr (f x).r_lt_R).ne') }
+  { change cont_diff_at ℝ n ((uncurry (some_cont_diff_bump_base E).to_fun) ∘
+      (λ (x : X),  ((f x).R / (f x).r, ((f x).r)⁻¹ • (g x - c x)))) x,
+    have A : ((f x).R / (f x).r, ((f x).r)⁻¹ • (g x - c x)) ∈ Ioi (1 : ℝ) ×ˢ (univ : set E),
+      by simpa only [prod_mk_mem_set_prod_eq, mem_univ, and_true] using (f x).one_lt_R_div_r,
+    have B : Ioi (1 : ℝ) ×ˢ (univ : set E) ∈ 𝓝 ((f x).R / (f x).r, (f x).r⁻¹ • (g x - c x)),
+      from (is_open_Ioi.prod is_open_univ).mem_nhds A,
+    apply ((((some_cont_diff_bump_base E).smooth.cont_diff_within_at A).cont_diff_at B)
+      .of_le le_top).comp x _,
+    exact (hR.div hr (f x).r_pos.ne').prod ((hr.inv (f x).r_pos.ne').smul (hg.sub hc)) }
 end
 
-lemma _root_.cont_diff.cont_diff_bump {c g : X → E} {f : ∀ x, cont_diff_bump_of_inner (c x)}
+lemma _root_.cont_diff.cont_diff_bump {c g : X → E} {f : ∀ x, cont_diff_bump (c x)}
   (hc : cont_diff ℝ n c) (hr : cont_diff ℝ n (λ x, (f x).r)) (hR : cont_diff ℝ n (λ x, (f x).R))
   (hg : cont_diff ℝ n g) : cont_diff ℝ n (λ x, f x (g x)) :=
 by { rw [cont_diff_iff_cont_diff_at] at *, exact λ x, (hc x).cont_diff_bump (hr x) (hR x) (hg x) }
@@ -419,7 +513,7 @@ f.continuous.div_const
 lemma normed_sub (x : E) : f.normed μ (c - x) = f.normed μ (c + x) :=
 by simp_rw [f.normed_def, f.sub]
 
-lemma normed_neg (f : cont_diff_bump_of_inner (0 : E)) (x : E) : f.normed μ (- x) = f.normed μ x :=
+lemma normed_neg (f : cont_diff_bump (0 : E)) (x : E) : f.normed μ (- x) = f.normed μ x :=
 by simp_rw [f.normed_def, f.neg]
 
 variables [borel_space E] [finite_dimensional ℝ E] [is_locally_finite_measure μ]
@@ -441,13 +535,13 @@ end
 
 lemma integral_normed : ∫ x, f.normed μ x ∂μ = 1 :=
 begin
-  simp_rw [cont_diff_bump_of_inner.normed, div_eq_mul_inv, mul_comm (f _), ← smul_eq_mul,
+  simp_rw [cont_diff_bump.normed, div_eq_mul_inv, mul_comm (f _), ← smul_eq_mul,
     integral_smul],
   exact inv_mul_cancel (f.integral_pos.ne')
 end
 
 lemma support_normed_eq : support (f.normed μ) = metric.ball c f.R :=
-by simp_rw [cont_diff_bump_of_inner.normed, support_div, f.support_eq,
+by simp_rw [cont_diff_bump.normed, support_div, f.support_eq,
   support_const f.integral_pos.ne', inter_univ]
 
 lemma tsupport_normed_eq : tsupport (f.normed μ) = metric.closed_ball c f.R :=
@@ -456,7 +550,7 @@ by simp_rw [tsupport, f.support_normed_eq, closure_ball _ f.R_pos.ne']
 lemma has_compact_support_normed : has_compact_support (f.normed μ) :=
 by simp_rw [has_compact_support, f.tsupport_normed_eq, is_compact_closed_ball]
 
-lemma tendsto_support_normed_small_sets {ι} {φ : ι → cont_diff_bump_of_inner c} {l : filter ι}
+lemma tendsto_support_normed_small_sets {ι} {φ : ι → cont_diff_bump c} {l : filter ι}
   (hφ : tendsto (λ i, (φ i).R) l (𝓝 0)) :
   tendsto (λ i, support (λ x, (φ i).normed μ x)) l (𝓝 c).small_sets :=
 begin
@@ -471,118 +565,8 @@ begin
 end
 
 variable (μ)
-lemma integral_normed_smul (z : X) [complete_space X] : ∫ x, f.normed μ x • z ∂μ = z :=
+lemma integral_normed_smul [complete_space X] (z : X) :
+  ∫ x, f.normed μ x • z ∂μ = z :=
 by simp_rw [integral_smul_const, f.integral_normed, one_smul]
 
-end cont_diff_bump_of_inner
-
-/-- `f : cont_diff_bump c`, where `c` is a point in a finite dimensional real vector space, is
-a bundled smooth function such that
-
-  - `f` is equal to `1` in `euclidean.closed_ball c f.r`;
-  - `support f = euclidean.ball c f.R`;
-  - `0 ≤ f x ≤ 1` for all `x`.
-
-The structure `cont_diff_bump` contains the data required to construct the function: real
-numbers `r`, `R`, and proofs of `0 < r < R`. The function itself is available through `coe_fn`.-/
-structure cont_diff_bump [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E]
-  (c : E)
-  extends cont_diff_bump_of_inner (to_euclidean c)
-
-namespace cont_diff_bump
-
-variables [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E}
-  (f : cont_diff_bump c)
-
-/-- The function defined by `f : cont_diff_bump c`. Use automatic coercion to function
-instead. -/
-def to_fun (f : cont_diff_bump c) : E → ℝ := f.to_cont_diff_bump_of_inner ∘ to_euclidean
-
-instance : has_coe_to_fun (cont_diff_bump c) (λ _, E → ℝ) := ⟨to_fun⟩
-
-instance (c : E) : inhabited (cont_diff_bump c) := ⟨⟨default⟩⟩
-
-lemma R_pos : 0 < f.R := f.to_cont_diff_bump_of_inner.R_pos
-
-lemma coe_eq_comp : ⇑f = f.to_cont_diff_bump_of_inner ∘ to_euclidean := rfl
-
-lemma one_of_mem_closed_ball (hx : x ∈ euclidean.closed_ball c f.r) :
-  f x = 1 :=
-f.to_cont_diff_bump_of_inner.one_of_mem_closed_ball hx
-
-lemma nonneg : 0 ≤ f x := f.to_cont_diff_bump_of_inner.nonneg
-
-lemma le_one : f x ≤ 1 := f.to_cont_diff_bump_of_inner.le_one
-
-lemma pos_of_mem_ball (hx : x ∈ euclidean.ball c f.R) : 0 < f x :=
-f.to_cont_diff_bump_of_inner.pos_of_mem_ball hx
-
-lemma lt_one_of_lt_dist (h : f.r < euclidean.dist x c) : f x < 1 :=
-f.to_cont_diff_bump_of_inner.lt_one_of_lt_dist h
-
-lemma zero_of_le_dist (hx : f.R ≤ euclidean.dist x c) : f x = 0 :=
-f.to_cont_diff_bump_of_inner.zero_of_le_dist hx
-
-lemma support_eq : support (f : E → ℝ) = euclidean.ball c f.R :=
-by rw [euclidean.ball_eq_preimage, ← f.to_cont_diff_bump_of_inner.support_eq,
-  ← support_comp_eq_preimage, coe_eq_comp]
-
-lemma tsupport_eq : tsupport f = euclidean.closed_ball c f.R :=
-by rw [tsupport, f.support_eq, euclidean.closure_ball _ f.R_pos.ne']
-
-protected lemma has_compact_support : has_compact_support f :=
-by simp_rw [has_compact_support, f.tsupport_eq, euclidean.is_compact_closed_ball]
-
-lemma eventually_eq_one_of_mem_ball (h : x ∈ euclidean.ball c f.r) :
-  f =ᶠ[𝓝 x] 1 :=
-to_euclidean.continuous_at (f.to_cont_diff_bump_of_inner.eventually_eq_one_of_mem_ball h)
-
-lemma eventually_eq_one : f =ᶠ[𝓝 c] 1 :=
-f.eventually_eq_one_of_mem_ball $ euclidean.mem_ball_self f.r_pos
-
-protected lemma cont_diff {n} :
-  cont_diff ℝ n f :=
-f.to_cont_diff_bump_of_inner.cont_diff.comp (to_euclidean : E ≃L[ℝ] _).cont_diff
-
-protected lemma cont_diff_at {n} :
-  cont_diff_at ℝ n f x :=
-f.cont_diff.cont_diff_at
-
-protected lemma cont_diff_within_at {s n} :
-  cont_diff_within_at ℝ n f s x :=
-f.cont_diff_at.cont_diff_within_at
-
-lemma exists_tsupport_subset {s : set E} (hs : s ∈ 𝓝 c) :
-  ∃ f : cont_diff_bump c, tsupport f ⊆ s :=
-let ⟨R, h0, hR⟩ := euclidean.nhds_basis_closed_ball.mem_iff.1 hs
-in ⟨⟨⟨R / 2, R, half_pos h0, half_lt_self h0⟩⟩, by rwa tsupport_eq⟩
-
-lemma exists_closure_subset {R : ℝ} (hR : 0 < R)
-  {s : set E} (hs : is_closed s) (hsR : s ⊆ euclidean.ball c R) :
-  ∃ f : cont_diff_bump c, f.R = R ∧ s ⊆ euclidean.ball c f.r :=
-begin
-  rcases euclidean.exists_pos_lt_subset_ball hR hs hsR with ⟨r, hr, hsr⟩,
-  exact ⟨⟨⟨r, R, hr.1, hr.2⟩⟩, rfl, hsr⟩
-end
-
 end cont_diff_bump
-
-open finite_dimensional metric
-
-/-- If `E` is a finite dimensional normed space over `ℝ`, then for any point `x : E` and its
-neighborhood `s` there exists an infinitely smooth function with the following properties:
-
-* `f y = 1` in a neighborhood of `x`;
-* `f y = 0` outside of `s`;
-*  moreover, `tsupport f ⊆ s` and `f` has compact support;
-* `f y ∈ [0, 1]` for all `y`.
-
-This lemma is a simple wrapper around lemmas about bundled smooth bump functions, see
-`cont_diff_bump`. -/
-lemma exists_cont_diff_bump_function_of_mem_nhds [normed_add_comm_group E] [normed_space ℝ E]
-  [finite_dimensional ℝ E] {x : E} {s : set E} (hs : s ∈ 𝓝 x) :
-  ∃ f : E → ℝ, f =ᶠ[𝓝 x] 1 ∧ (∀ y, f y ∈ Icc (0 : ℝ) 1) ∧ cont_diff ℝ ⊤ f ∧
-    has_compact_support f ∧ tsupport f ⊆ s :=
-let ⟨f, hf⟩ := cont_diff_bump.exists_tsupport_subset hs in
-⟨f, f.eventually_eq_one, λ y, ⟨f.nonneg, f.le_one⟩, f.cont_diff,
-  f.has_compact_support, hf⟩
diff --git a/src/analysis/convolution.lean b/src/analysis/convolution.lean
index f21b490b15f2e..be505012c1379 100644
--- a/src/analysis/convolution.lean
+++ b/src/analysis/convolution.lean
@@ -6,8 +6,8 @@ Authors: Floris van Doorn
 import measure_theory.group.integration
 import measure_theory.group.prod
 import measure_theory.function.locally_integrable
+import analysis.calculus.bump_function_inner
 import measure_theory.integral.interval_integral
-import analysis.calculus.specific_functions
 import analysis.calculus.parametric_integral
 
 /-!
@@ -66,7 +66,7 @@ Versions of these statements for functions depending on a parameter are also giv
 
 * `convolution_tendsto_right`: Given a sequence of nonnegative normalized functions whose support
   tends to a small neighborhood around `0`, the convolution tends to the right argument.
-  This is specialized to bump functions in `cont_diff_bump_of_inner.convolution_tendsto_right`.
+  This is specialized to bump functions in `cont_diff_bump.convolution_tendsto_right`.
 
 # Notation
 The following notations are localized in the locale `convolution`:
@@ -902,7 +902,7 @@ end
 * `g i x` tends to `z₀` as `(i, x)` tends to `l ×ᶠ 𝓝 x₀`;
 * `k i` tends to `x₀`.
 
-See also `cont_diff_bump_of_inner.convolution_tendsto_right`.
+See also `cont_diff_bump.convolution_tendsto_right`.
 -/
 lemma convolution_tendsto_right
   {ι} {g : ι → G → E'} {l : filter ι} {x₀ : G} {z₀ : E'}
@@ -937,13 +937,13 @@ end
 
 end normed_add_comm_group
 
-namespace cont_diff_bump_of_inner
+namespace cont_diff_bump
 
 variables {n : ℕ∞}
 variables [normed_space ℝ E']
-variables [inner_product_space ℝ G]
+variables [normed_add_comm_group G] [normed_space ℝ G] [has_cont_diff_bump G]
 variables [complete_space E']
-variables {a : G} {φ : cont_diff_bump_of_inner (0 : G)}
+variables {a : G} {φ : cont_diff_bump (0 : G)}
 
 /-- If `φ` is a bump function, compute `(φ ⋆ g) x₀` if `g` is constant on `metric.ball x₀ φ.R`. -/
 lemma convolution_eq_right {x₀ : G}
@@ -976,7 +976,7 @@ dist_convolution_le (by simp_rw [← dist_self (g x₀), hg x₀ (mem_ball_self
 * `g i` is `mu`-a.e. strongly measurable as `i` tends to `l`;
 * `g i x` tends to `z₀` as `(i, x)` tends to `l ×ᶠ 𝓝 x₀`;
 * `k i` tends to `x₀`. -/
-lemma convolution_tendsto_right {ι} {φ : ι → cont_diff_bump_of_inner (0 : G)}
+lemma convolution_tendsto_right {ι} {φ : ι → cont_diff_bump (0 : G)}
   {g : ι → G → E'} {k : ι → G} {x₀ : G} {z₀ : E'} {l : filter ι}
   (hφ : tendsto (λ i, (φ i).R) l (𝓝 0))
   (hig : ∀ᶠ i in l, ae_strongly_measurable (g i) μ)
@@ -987,16 +987,16 @@ convolution_tendsto_right (eventually_of_forall $ λ i, (φ i).nonneg_normed)
   (eventually_of_forall $ λ i, (φ i).integral_normed)
   (tendsto_support_normed_small_sets hφ) hig hcg hk
 
-/-- Special case of `cont_diff_bump_of_inner.convolution_tendsto_right` where `g` is continuous,
+/-- Special case of `cont_diff_bump.convolution_tendsto_right` where `g` is continuous,
   and the limit is taken only in the first function. -/
-lemma convolution_tendsto_right_of_continuous {ι} {φ : ι → cont_diff_bump_of_inner (0 : G)}
+lemma convolution_tendsto_right_of_continuous {ι} {φ : ι → cont_diff_bump (0 : G)}
   {l : filter ι} (hφ : tendsto (λ i, (φ i).R) l (𝓝 0))
   (hg : continuous g) (x₀ : G) :
   tendsto (λ i, ((λ x, (φ i).normed μ x) ⋆[lsmul ℝ ℝ, μ] g : G → E') x₀) l (𝓝 (g x₀)) :=
 convolution_tendsto_right hφ (eventually_of_forall $ λ _, hg.ae_strongly_measurable)
   ((hg.tendsto x₀).comp tendsto_snd) tendsto_const_nhds
 
-end cont_diff_bump_of_inner
+end cont_diff_bump
 
 end measurability
 
diff --git a/src/geometry/manifold/bump_function.lean b/src/geometry/manifold/bump_function.lean
index 999bcb4927999..80262412fa133 100644
--- a/src/geometry/manifold/bump_function.lean
+++ b/src/geometry/manifold/bump_function.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import analysis.calculus.specific_functions
+import analysis.calculus.bump_function_findim
 import geometry.manifold.cont_mdiff
 
 /-!
@@ -14,8 +14,8 @@ In this file we define `smooth_bump_function I c` to be a bundled smooth "bump"
 define a coercion to function for this type, and for `f : smooth_bump_function I c`, the function
 `⇑f` written in the extended chart at `c` has the following properties:
 
-* `f x = 1` in the closed euclidean ball of radius `f.r` centered at `c`;
-* `f x = 0` outside of the euclidean ball of radius `f.R` centered at `c`;
+* `f x = 1` in the closed ball of radius `f.r` centered at `c`;
+* `f x = 0` outside of the ball of radius `f.R` centered at `c`;
 * `0 ≤ f x ≤ 1` for all `x`.
 
 The actual statements involve (pre)images under `ext_chart_at I f` and are given as lemmas in the
@@ -32,7 +32,7 @@ variables
 {H : Type uH} [topological_space H] (I : model_with_corners ℝ E H)
 {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
 
-open function filter finite_dimensional set
+open function filter finite_dimensional set metric
 open_locale topology manifold classical filter big_operators
 
 noncomputable theory
@@ -47,8 +47,8 @@ In this section we define a structure for a bundled smooth bump function and pro
 `f : smooth_bump_function I M` is a smooth function on `M` such that in the extended chart `e` at
 `f.c`:
 
-* `f x = 1` in the closed euclidean ball of radius `f.r` centered at `f.c`;
-* `f x = 0` outside of the euclidean ball of radius `f.R` centered at `f.c`;
+* `f x = 1` in the closed ball of radius `f.r` centered at `f.c`;
+* `f x = 0` outside of the ball of radius `f.R` centered at `f.c`;
 * `0 ≤ f x ≤ 1` for all `x`.
 
 The structure contains data required to construct a function with these properties. The function is
@@ -56,15 +56,12 @@ available as `⇑f` or `f x`. Formal statements of the properties listed above i
 (pre)images under `ext_chart_at I f.c` and are given as lemmas in the `smooth_bump_function`
 namespace. -/
 structure smooth_bump_function (c : M) extends cont_diff_bump (ext_chart_at I c c) :=
-(closed_ball_subset :
-  (euclidean.closed_ball (ext_chart_at I c c) R) ∩ range I ⊆ (ext_chart_at I c).target)
+(closed_ball_subset : (closed_ball (ext_chart_at I c c) R) ∩ range I ⊆ (ext_chart_at I c).target)
 
 variable {M}
 
 namespace smooth_bump_function
 
-open euclidean (renaming dist -> eudist)
-
 variables {c : M} (f : smooth_bump_function I c) {x : M} {I}
 
 /-- The function defined by `f : smooth_bump_function c`. Use automatic coercion to function
@@ -93,7 +90,7 @@ lemma eventually_eq_of_mem_source (hx : x ∈ (chart_at H c).source) :
 f.eq_on_source.eventually_eq_of_mem $ is_open.mem_nhds (chart_at H c).open_source hx
 
 lemma one_of_dist_le (hs : x ∈ (chart_at H c).source)
-  (hd : eudist (ext_chart_at I c x) (ext_chart_at I c c) ≤ f.r) :
+  (hd : dist (ext_chart_at I c x) (ext_chart_at I c c) ≤ f.r) :
   f x = 1 :=
 by simp only [f.eq_on_source hs, (∘), f.to_cont_diff_bump.one_of_mem_closed_ball hd]
 
@@ -149,7 +146,7 @@ lemma nonneg : 0 ≤ f x := f.mem_Icc.1
 lemma le_one : f x ≤ 1 := f.mem_Icc.2
 
 lemma eventually_eq_one_of_dist_lt (hs : x ∈ (chart_at H c).source)
-  (hd : eudist (ext_chart_at I c x) (ext_chart_at I c c) < f.r) :
+  (hd : dist (ext_chart_at I c x) (ext_chart_at I c c) < f.r) :
   f =ᶠ[𝓝 x] 1 :=
 begin
   filter_upwards [is_open.mem_nhds (is_open_ext_chart_at_preimage I c is_open_ball) ⟨hs, hd⟩],
@@ -159,7 +156,7 @@ end
 
 lemma eventually_eq_one : f =ᶠ[𝓝 c] 1 :=
 f.eventually_eq_one_of_dist_lt (mem_chart_source _ _) $
-by { rw [euclidean.dist, dist_self], exact f.r_pos }
+by { rw [dist_self], exact f.r_pos }
 
 @[simp] lemma eq_one : f c = 1 := f.eventually_eq_one.eq_of_nhds
 
@@ -173,9 +170,9 @@ lemma c_mem_support : c ∈ support f := mem_of_mem_nhds f.support_mem_nhds
 
 lemma nonempty_support : (support f).nonempty := ⟨c, f.c_mem_support⟩
 
-lemma compact_symm_image_closed_ball :
+lemma is_compact_symm_image_closed_ball :
   is_compact ((ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I)) :=
-(euclidean.is_compact_closed_ball.inter_right I.closed_range).image_of_continuous_on $
+((is_compact_closed_ball _ _).inter_right I.closed_range).image_of_continuous_on $
   (continuous_on_ext_chart_at_symm _ _).mono f.closed_ball_subset
 
 /-- Given a smooth bump function `f : smooth_bump_function I c`, the closed ball of radius `f.R` is
@@ -185,11 +182,11 @@ lemma nhds_within_range_basis :
   (𝓝[range I] (ext_chart_at I c c)).has_basis (λ f : smooth_bump_function I c, true)
     (λ f, closed_ball (ext_chart_at I c c) f.R ∩ range I) :=
 begin
-  refine ((nhds_within_has_basis euclidean.nhds_basis_closed_ball _).restrict_subset
+  refine ((nhds_within_has_basis nhds_basis_closed_ball _).restrict_subset
       (ext_chart_at_target_mem_nhds_within _ _)).to_has_basis' _ _,
   { rintro R ⟨hR0, hsub⟩,
-    exact ⟨⟨⟨⟨R / 2, R, half_pos hR0, half_lt_self hR0⟩⟩, hsub⟩, trivial, subset.rfl⟩ },
-  { exact λ f _, inter_mem (mem_nhds_within_of_mem_nhds $ closed_ball_mem_nhds f.R_pos)
+    exact ⟨⟨⟨R / 2, R, half_pos hR0, half_lt_self hR0⟩, hsub⟩, trivial, subset.rfl⟩ },
+  { exact λ f _, inter_mem (mem_nhds_within_of_mem_nhds $ closed_ball_mem_nhds _ f.R_pos)
       self_mem_nhds_within }
 end
 
@@ -199,7 +196,7 @@ begin
   rw f.image_eq_inter_preimage_of_subset_support hs,
   refine continuous_on.preimage_closed_of_closed
     ((continuous_on_ext_chart_at_symm _ _).mono f.closed_ball_subset) _ hsc,
-  exact is_closed.inter is_closed_closed_ball I.closed_range
+  exact is_closed.inter is_closed_ball I.closed_range
 end
 
 /-- If `f` is a smooth bump function and `s` closed subset of the support of `f` (i.e., of the open
@@ -212,13 +209,13 @@ begin
   set e := ext_chart_at I c,
   have : is_closed (e '' s) := f.is_closed_image_of_is_closed hsc hs,
   rw [support_eq_inter_preimage, subset_inter_iff, ← image_subset_iff] at hs,
-  rcases euclidean.exists_pos_lt_subset_ball f.R_pos this hs.2 with ⟨r, hrR, hr⟩,
+  rcases exists_pos_lt_subset_ball f.R_pos this hs.2 with ⟨r, hrR, hr⟩,
   exact ⟨r, hrR, subset_inter hs.1 (image_subset_iff.1 hr)⟩
 end
 
 /-- Replace `r` with another value in the interval `(0, f.R)`. -/
 def update_r (r : ℝ) (hr : r ∈ Ioo 0 f.R) : smooth_bump_function I c :=
-⟨⟨⟨r, f.R, hr.1, hr.2⟩⟩, f.closed_ball_subset⟩
+⟨⟨r, f.R, hr.1, hr.2⟩, f.closed_ball_subset⟩
 
 @[simp] lemma update_r_R {r : ℝ} (hr : r ∈ Ioo 0 f.R) : (f.update_r r hr).R = f.R := rfl
 
@@ -235,7 +232,7 @@ variables [t2_space M]
 
 lemma is_closed_symm_image_closed_ball :
   is_closed ((ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I)) :=
-f.compact_symm_image_closed_ball.is_closed
+f.is_compact_symm_image_closed_ball.is_closed
 
 lemma tsupport_subset_symm_image_closed_ball :
   tsupport f ⊆ (ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I) :=
@@ -260,7 +257,7 @@ lemma tsupport_subset_chart_at_source :
 by simpa only [ext_chart_at_source] using f.tsupport_subset_ext_chart_at_source
 
 protected lemma has_compact_support : has_compact_support f :=
-is_compact_of_is_closed_subset f.compact_symm_image_closed_ball is_closed_closure
+is_compact_of_is_closed_subset f.is_compact_symm_image_closed_ball is_closed_closure
  f.tsupport_subset_symm_image_closed_ball
 
 variables (I c)