∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {D : ℝ} {x : E},
  0 < D → x ∈ Metric.closedBall 0 (1 - D) → ExistsContDiffBumpBase.y D x = 1