α : Type u_1
β : Type u_2
γ : Type ?u.64319
δ : Type ?u.64322
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type ?u.64355
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
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F s hs) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
s : Set α
hs : s ∈ A
x : ↑s
x' : ↑↑{ val := s, property := hs } := x
⊢ ↑(let S := Subtype.val;
        let F_1 := fun i => F ↑i (_ : ↑i ∈ A);
        liftCover S F_1
          (_ :
            ∀ (i j : ↑A) (x : α) (hxi : x ∈ ↑i) (hxj : x ∈ ↑j),
              ↑(F ↑i (_ : ↑i ∈ A)) { val := x, property := hxi } = ↑(F ↑j (_ : ↑j ∈ A)) { val := x, property := hxj })
          (_ : ∀ (x : α), ∃ i, ↑i ∈ nhds x))
      ↑x =
    ↑(F s hs) x
α : Type u_1
β : Type u_2
γ : Type ?u.64319
δ : Type ?u.64322
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type ?u.64355
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
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F s hs) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
s : Set α
hs : s ∈ A
x : ↑s
x' : ↑↑{ val := s, property := hs } := x
⊢ ↑(liftCover' A F hF hA) ↑x = ↑(F s hs) x
delta liftCover'
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.64319
δ : Type ?u.64322
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type ?u.64355
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
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    ↑(F s hs) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }
hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x
s : Set α
hs : s ∈ A
x : ↑s
x' : ↑↑{ val := s, property := hs } := x
⊢ ↑(let S := Subtype.val;
        let F_1 := fun i => F ↑i (_ : ↑i ∈ A);
        liftCover S F_1
          (_ :
            ∀ (i j : ↑A) (x : α) (hxi : x ∈ ↑i) (hxj : x ∈ ↑j),
              ↑(F ↑i (_ : ↑i ∈ A)) { val := x, property := hxi } = ↑(F ↑j (_ : ↑j ∈ A)) { val := x, property := hxj })
          (_ : ∀ (x : α), ∃ i, ↑i ∈ nhds x))
      ↑x =
    ↑(F s hs) x
exact liftCover_coe x'