chore(Analysis/Calculus): golf IsOpen.exists_smooth_support_eq using grind (#27723)

Author: euprunin

Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

@@ -113,10 +113,7 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
     rw [← hT] at hx
     obtain ⟨i, iT, hi⟩ : ∃ i ∈ T, x ∈ support (i : E → ℝ) := by
       simpa only [mem_iUnion, exists_prop] using hx
-    rw [hg, mem_range] at iT
-    rcases iT with ⟨n, hn⟩
-    rw [← hn] at hi
-    exact ⟨n, hi⟩
+    grind [Set.mem_range]
   have g_smooth : ∀ n, ContDiff ℝ ∞ (g n) := fun n => (g0 n).2.2.2.1
   have g_comp_supp : ∀ n, HasCompactSupport (g n) := fun n => (g0 n).2.2.1
   have g_nonneg : ∀ n x, 0 ≤ g n x := fun n x => ((g0 n).2.2.2.2 (mem_range_self x)).1