-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_isSubordinate [T2Space M] [SigmaCompactSpace M] (hs : IsClosed s)
    (hU : ∀ x ∈ s, U x ∈ 𝓝 x) :
    ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate U

Proof state:
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
⊢ ∃ ι f, f.IsSubordinate U

Tactic:
haveI : LocallyCompactSpace H := I.locallyCompactSpace

Result:
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this : LocallyCompactSpace H
⊢ ∃ ι f, f.IsSubordinate U

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.refine_2
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ a, support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι), V i ⊆ (chartAt H (c i)).source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
x : M
hx : x ∈ s
⊢ ∃ i, ↑((fun i => (f i).updateRIn (r i) ⋯) i) =ᶠ[𝓝 x] 1

Tactic:
refine (mem_iUnion.1 <| hsV hx).imp fun i hi => ?_

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.refine_2
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ a, support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι), V i ⊆ (chartAt H (c i)).source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
x : M
hx : x ∈ s
i : ι
hi : x ∈ V i
⊢ ↑((fun i => (f i).updateRIn (r i) ⋯) i) =ᶠ[𝓝 x] 1

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.refine_2
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ a, support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι), V i ⊆ (chartAt H (c i)).source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
x : M
hx : x ∈ s
i : ι
hi : x ∈ V i
⊢ ↑((fun i => (f i).updateRIn (r i) ⋯) i) =ᶠ[𝓝 x] 1

Tactic:
exact ((f i).updateRIn _ _).eventuallyEq_one_of_dist_lt
  ((f i).support_subset_source <| hVf _ hi) (hr i hi).2

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.refine_3
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ a, support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι), V i ⊆ (chartAt H (c i)).source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
i : ι
⊢ tsupport
      ↑({ c := c, toFun := fun i => (f i).updateRIn (r i) ⋯, c_mem' := hcs, locallyFinite' := ⋯,
              eventuallyEq_one' := ⋯ }.toFun
          i) ⊆
    U
      ({ c := c, toFun := fun i => (f i).updateRIn (r i) ⋯, c_mem' := hcs, locallyFinite' := ⋯,
            eventuallyEq_one' := ⋯ }.c
        i)

Tactic:
simpa only [SmoothBumpFunction.support_updateRIn, tsupport] using hfU i

Result:
no goals