-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
    ∃ f : E → ℝ, f.support = s ∧ ContDiff ℝ ∞ f ∧ Set.range f ⊆ Set.Icc 0 1

Proof state:
case inr.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n => ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
⊢ ∃ f, support f = s ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1

Tactic:
have : ∀ n : ℕ, ∃ r : ℝ, 0 < r ∧ ∀ i ≤ n, ∀ x, ‖iteratedFDeriv ℝ i (r • g n) x‖ ≤ δ n := by
  intro n
  have : ∀ i, ∃ R, ∀ x, ‖iteratedFDeriv ℝ i (fun x => g n x) x‖ ≤ R := by
    intro i
    have : BddAbove (range fun x => ‖iteratedFDeriv ℝ i (fun x : E => g n x) x‖) := by
      apply ((g_smooth n).continuous_iteratedFDeriv
        (mod_cast le_top)).norm.bddAbove_range_of_hasCompactSupport
      apply HasCompactSupport.comp_left _ norm_zero
      apply (g_comp_supp n).iteratedFDeriv
    rcases this with ⟨R, hR⟩
    exact ⟨R, fun x => hR (mem_range_self _)⟩
  choose R hR using this
  let M := max (((Finset.range (n + 1)).image R).max' (by simp)) 1
  have δnpos : 0 < δ n := δpos n
  have IR : ∀ i ≤ n, R i ≤ M := by
    intro i hi
    refine le_trans ?_ (le_max_left _ _)
    apply Finset.le_max'
    apply Finset.mem_image_of_mem
    simpa only [Finset.mem_range, Nat.lt_add_one_iff]
  refine ⟨M⁻¹ * δ n, by positivity, fun i hi x => ?_⟩
  calc
    ‖iteratedFDeriv ℝ i ((M⁻¹ * δ n) • g n) x‖ = ‖(M⁻¹ * δ n) • iteratedFDeriv ℝ i (g n) x‖ := by
      rw [iteratedFDeriv_const_smul_apply]
      exact (g_smooth n).contDiffAt.of_le (mod_cast le_top)
    _ = M⁻¹ * δ n * ‖iteratedFDeriv ℝ i (g n) x‖ := by
      rw [norm_smul _ (iteratedFDeriv ℝ i (g n) x), Real.norm_of_nonneg]; positivity
    _ ≤ M⁻¹ * δ n * M := by gcongr; exact (hR i x).trans (IR i hi)
    _ = δ n := by field_simp

Result:
case inr.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n => ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
this : ∀ (n : ℕ), ∃ r, 0 < r ∧ ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i (r • g n) x‖ ≤ ↑(δ n)
⊢ ∃ f, support f = s ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1

Proof state:
case H.mk
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
this : ⋃ f, support ↑f = s
f : E → ℝ
hf : support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1
⊢ IsOpen (support ↑⟨f, hf⟩)

Tactic:
exact hf.2.2.1.continuous.isOpen_support

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro.intro.intro.intro.refine_1.h₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n => ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n => (r n • g n) x
x : E
hx : x ∉ s
this : ∀ (n : ℕ), g n x = 0
⊢ ∑' (n : ℕ), r n * g n x = 0

Tactic:
simp only [this, mul_zero, tsum_zero]

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro.intro.intro.intro.refine_3.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n => ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n => (r n • g n) x
y : E
⊢ (fun x => ∑' (n : ℕ), (r n • g n) x) y ≤ (fun a => ↑a) c

Tactic:
have A : HasSum (fun n => (δ n : ℝ)) c := NNReal.hasSum_coe.2 δc

Result:
case inr.intro.intro.intro.intro.intro.intro.intro.refine_3.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n => ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n => (r n • g n) x
y : E
A : HasSum (fun n => ↑(δ n)) ↑c
⊢ (fun x => ∑' (n : ℕ), (r n • g n) x) y ≤ (fun a => ↑a) c