case h
α : Type u_1
β : Type u_2
γ : Type ?u.58521
δ : Type ?u.58524
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 : ι
a✝ : ↑(S i)
⊢ ↑(restrict (S i) (liftCover S φ hφ hS)) a✝ = ↑(φ i) a✝
α : Type u_1
β : Type u_2
γ : Type ?u.58521
δ : Type ?u.58524
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 : ι
⊢ restrict (S i) (liftCover S φ hφ hS) = φ i
ext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.58521
δ : Type ?u.58524
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 : ι
a✝ : ↑(S i)
⊢ ↑(restrict (S i) (liftCover S φ hφ hS)) a✝ = ↑(φ i) a✝
simp only [coe_restrict, Function.comp_apply, liftCover_coe]