-- Mathlib/Topology/PartitionOfUnity.lean
theorem exists_isSubordinate_of_locallyFinite_of_prop [NormalSpace X] (p : (X → ℝ) → Prop)
    (h01 : ∀ s t, IsClosed s → IsClosed t → Disjoint s t →
      ∃ f : C(X, ℝ), p f ∧ EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1)
    (hs : IsClosed 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

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed 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
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
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

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)⟩

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed 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
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
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.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed 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
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
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

Tactic:
rcases mem_iUnion.1 (hsW hx) with ⟨i, hi⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed 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
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
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

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed 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
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
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

Tactic:
have hsupp : ∀ i, support (f i) ⊆ V i := fun i => support_subset_iff'.2 (hf0 i)

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed 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
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
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