-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (ho : ∀ i, IsOpen (U i))
    (hU : s ⊆ ⋃ i, U i) : ∃ f : SmoothPartitionOfUnity ι I M s, f.IsSubordinate U

Proof state:
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ ∃ f, f.IsSubordinate U

Tactic:
have := BumpCovering.exists_isSubordinate_of_prop (ContMDiff I 𝓘(ℝ) ∞) ?_ hs U ho hU

Result:
case refine_2
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : ∃ f, (∀ (i : ι), ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑(f i)) ∧ f.IsSubordinate U
⊢ ∃ f, f.IsSubordinate U

case refine_1
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ ∀ (s t : Set M),
    IsClosed s →
      IsClosed t →
        Disjoint s t → ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Proof state:
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
this : LocallyCompactSpace H
⊢ ∃ f, f.IsSubordinate U

Tactic:
haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M

Result:
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ ∃ f, f.IsSubordinate U

Proof state:
case refine_1
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ ∀ (s t : Set M),
    IsClosed s →
      IsClosed t →
        Disjoint s t → ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
intro s t hs ht hd

Result:
case refine_1
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s✝ : Set M
hs✝ : IsClosed s✝
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s✝ ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Proof state:
case refine_1
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s✝ : Set M
hs✝ : IsClosed s✝
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s✝ ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
rcases exists_smooth_zero_one_of_isClosed I hs ht hd with ⟨f, hf⟩

Result:
case refine_1.intro
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s✝ : Set M
hs✝ : IsClosed s✝
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s✝ ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
f : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hf : EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Proof state:
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
⊢ ∃ f, f.IsSubordinate U

Tactic:
haveI : LocallyCompactSpace H := I.locallyCompactSpace

Result:
ι : Type uι
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
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
this : LocallyCompactSpace H
⊢ ∃ f, f.IsSubordinate U