-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem exists_smooth_tsupport_subset {s : Set E} {x : E} (hs : s ∈ 𝓝 x) :
    ∃ f : E → ℝ,
      tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1

Proof state:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ ∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1

Tactic:
refine ⟨f, f_tsupp.trans hd, ?_, ?_, ?_, ?_⟩

Result:
case intro.intro.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ HasCompactSupport f

case intro.intro.refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ ContDiff ℝ ∞ f

case intro.intro.refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ range f ⊆ Icc 0 1

case intro.intro.refine_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ f x = 1

Proof state:
case intro.intro.refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ ContDiff ℝ ∞ f

Tactic:
apply c.contDiff.comp

Result:
case intro.intro.refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ ContDiff ℝ ∞ ⇑toEuclidean

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
⊢ closure (support f) ⊆ closure (Euclidean.ball x d)

Tactic:
exact closure_mono f_supp

Result:
no goals

Proof state:
case intro.intro.refine_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ toEuclidean x ∈ closedBall (toEuclidean x) c.rIn

Tactic:
apply mem_closedBall_self

Result:
case intro.intro.refine_4.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ 0 ≤ c.rIn

Proof state:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
⊢ ∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1

Tactic:
let c : ContDiffBump (toEuclidean x) :=
  { rIn := d / 2
    rOut := d
    rIn_pos := half_pos d_pos
    rIn_lt_rOut := half_lt_self d_pos }

Result:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
⊢ ∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1

Proof state:
case intro.intro.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ Bornology.IsBounded (tsupport f)

Tactic:
have : IsBounded (Euclidean.closedBall x d) := Euclidean.isCompact_closedBall.isBounded

Result:
case intro.intro.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
this : Bornology.IsBounded (Euclidean.closedBall x d)
⊢ Bornology.IsBounded (tsupport f)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
y : E
hy : y ∈ support f
⊢ y ∈ Euclidean.ball x d

Tactic:
have : toEuclidean y ∈ Function.support c := by
  simpa only [Function.mem_support, Function.comp_apply, Ne] using hy

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
y : E
hy : y ∈ support f
this : toEuclidean y ∈ support ↑c
⊢ y ∈ Euclidean.ball x d