-- Mathlib/Topology/PartitionOfUnity.lean
theorem exists_isSubordinate_of_locallyFinite_of_prop_t2space [LocallyCompactSpace X] [T2Space X]
    (p : (X → ℝ) → Prop) (h01 : ∀ s t, IsClosed s → IsCompact t → Disjoint s t → ∃ f : C(X, ℝ),
    p f ∧ EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1)
    (hs : IsCompact s) (U : ι → Set X) (ho : ∀ i, IsOpen (U i)) (hf : LocallyFinite U)
    (hU : s ⊆ ⋃ i, U i) :
    ∃ f : BumpCovering ι X s, (∀ i, p (f i)) ∧ f.IsSubordinate U ∧
      ∀ i, HasCompactSupport (f i)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsCompact t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure (W i))
⊢ ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)

Tactic:
choose f hfp hf0 hf1 hf01 using fun i =>
  h01 _ _ (isClosed_compl_iff.2 <| hVo i) (hWc i)
    (disjoint_right.2 fun x hx => Classical.not_not.2 (hWV i hx))

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsCompact t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure (W i))
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ⇑(f i)
hf0 : ∀ (i : ι), EqOn (⇑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (⇑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), (f i) x ∈ Icc 0 1
⊢ ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsCompact t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure (W i))
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ⇑(f i)
hf0 : ∀ (i : ι), EqOn (⇑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (⇑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), (f i) x ∈ Icc 0 1
hsupp : ∀ (i : ι), support ⇑(f i) ⊆ V i
x : X
hx : x ∈ s
i : ι
hi : x ∈ W i
⊢ ∃ i, ⇑(f i) =ᶠ[𝓝 x] 1

Tactic:
exact ⟨i, ((hf1 i).mono subset_closure).eventuallyEq_of_mem ((hWo i).mem_nhds hi)⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsCompact t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure (W i))
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ⇑(f i)
hf0 : ∀ (i : ι), EqOn (⇑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (⇑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), (f i) x ∈ Icc 0 1
hsupp : ∀ (i : ι), support ⇑(f i) ⊆ V i
⊢ ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)

Tactic:
refine ⟨⟨f, hf.subset fun i => Subset.trans (hsupp i) (hVU' i), fun i x => (hf01 i x).1,
    fun i x => (hf01 i x).2, fun x hx => ?_⟩,
  hfp, fun i => Subset.trans (closure_mono (hsupp i)) (hVU i),
  fun i => IsCompact.of_isClosed_subset (hcp i) isClosed_closure <| closure_mono (hsupp i)⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsCompact t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure (W i))
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ⇑(f i)
hf0 : ∀ (i : ι), EqOn (⇑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (⇑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), (f i) x ∈ Icc 0 1
hsupp : ∀ (i : ι), support ⇑(f i) ⊆ V i
x : X
hx : x ∈ s
⊢ ∃ i, ⇑(f i) =ᶠ[𝓝 x] 1

Proof state:
case intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsCompact t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure (V i))
⊢ ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)

Tactic:
have hVU' i : V i ⊆ U i := subset_closure.trans (hVU i)

Result:
case intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsCompact t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)