theorem exists_contDiff_one_nhds_of_interior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s t : Set E} (hs : IsClosed s) (hd : s ⊆ interior t) : ∃ (f : E → ℝ), ContDiff ℝ (↑⊤) f ∧ (∀ᶠ (x : E) in nhdsSet s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ (x : E), f x ∈ Set.Icc 0 1