no goals
α : Type u_1
β : Type u_2
γ : Type ?u.56918
δ : Type ?u.56921
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_3
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    ↑(φ i) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }
hS : ∀ (x : α), ∃ i, S i ∈ nhds x
i : ι
x : ↑(S i)
⊢ ↑(liftCover S φ hφ hS) ↑x = ↑(φ i) x
rw [liftCover, coe_mk, Set.liftCover_coe _]