Exists unit Ball cutoff

lemma exists_unitBall_cutoff :    ∃ (φ : E → ℝ),      ContDiff ℝ (⊤ : ℕ∞) φ ∧      HasCompactSupport φ ∧      tsupport φ ⊆ Metric.ball (0 : E) (7 / 6 : ℝ) ∧      (∀ x ∈ Metric.closedBall (0 : E) 1, φ x = 1) ∧      Set.range φ ⊆ Set.Icc (0 : ℝ) 1 := by  have hK : IsCompact (Metric.closedBall (0 : E) 1) := isCompact_closedBall 0 1  have hΩ : IsOpen (Metric.ball (0 : E) (7 / 6 : ℝ)) := isOpen_ball  have hKΩ : Metric.closedBall (0 : E) 1 ⊆ Metric.ball (0 : E) (7 / 6 : ℝ) :=    Metric.closedBall_subset_ball (by norm_num : (1 : ℝ) < 7 / 6)  obtain ⟨δ, hδ_pos, hδΩ⟩ := hK.exists_cthickening_subset_open hΩ hKΩ  rcases exists_contMDiff_support_eq_eq_one_iff      (I := modelWithCornersSelf ℝ E) (s := Metric.thickening δ (Metric.closedBall (0 : E) 1))      (t := Metric.closedBall (0 : E) 1)      isOpen_thickening isClosed_closedBall      (self_subset_thickening hδ_pos (Metric.closedBall (0 : E) 1)) with    ⟨η, hη_smooth, hη_range, hη_support, hη_one_iff⟩  refine ⟨η, contMDiff_iff_contDiff.mp hη_smooth, ?_, ?_, ?_, hη_range⟩  · apply HasCompactSupport.intro' (K := Metric.cthickening δ (Metric.closedBall (0 : E) 1))    · exact (isCompact_closedBall 0 1).cthickening (r := δ)    · exact isClosed_cthickening    · intro x hx      have hxt : x ∉ tsupport η := by        intro hxt        have hx_closure : x ∈ closure (Metric.thickening δ (Metric.closedBall (0 : E) 1)) := by          rw [tsupport, hη_support] at hxt; exact hxt        exact hx (Metric.closure_thickening_subset_cthickening δ _ hx_closure)      exact image_eq_zero_of_notMem_tsupport hxt  · rw [tsupport, hη_support]    exact (Metric.closure_thickening_subset_cthickening δ _).trans hδΩ  · intro x hx; exact (hη_one_iff x).1 hx