-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
x : (↑(h.U i) : Type u)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
w :
  Eq (α :=
    { p :
      (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
        (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
      (↑p.1 : (↑(h.U i) : Type u)) = (↑p.2 : (↑(h.U i) : Type u)) })
    (Subtype.mk (p :=
        fun
          (p :
            (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
              (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u)) ↦
        (↑p.1 : (↑(h.U i) : Type u)) = (↑p.2 : (↑(h.U i) : Type u)))
        (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j)
            (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (h.t k i) :
                    (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) →
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u))
                  (Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
                    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) (h.t j k) :
                            (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                              (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
                          (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
                            (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                      (CC := carrier) (h.t i j) :
                                    (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
                                      (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
                                  (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                              (↑(h.U j) : Type u))
                            ⋯)) :
                      (↑(h.U k) : Type u))
                    ⋯)) :
              (↑(h.U i) : Type u))
            ⋯,
          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.t k i) :
              (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) →
                (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u))
            (Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
              (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (h.t j k) :
                      (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                        (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
                    (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
                      (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (h.t i j) :
                              (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
                                (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
                            (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                        (↑(h.U j) : Type u))
                      ⋯)) :
                (↑(h.U k) : Type u))
              ⋯))
        ⋯ :
      { p :
        (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
          (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
        (↑p.1 : (↑(h.U i) : Type u)) = (↑p.2 : (↑(h.U i) : Type u)) })
    (Subtype.mk (p :=
        fun
          (p :
            (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
              (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u)) ↦
        (↑p.1 : (↑(h.U i) : Type u)) = (↑p.2 : (↑(h.U i) : Type u)))
        (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx,
          Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')
        ⋯ :
      { p :
        (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
          (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
        (↑p.1 : (↑(h.U i) : Type u)) = (↑p.2 : (↑(h.U i) : Type u)) })
⊢ Eq (α :=
    (↑(of
          { p :
            (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
              (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
            Eq (α := (↑(h.U i) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (h.V i j).inclusion' :
                    (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                  p.1 :
                (↑(h.U i) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (h.V i k).inclusion' :
                    (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                  p.2 :
                (↑(h.U i) : Type u)) }) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (ofHom
                {
                  toFun :=
                    fun
                      (x :
                        { p :
                          (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
                            (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
                          Eq (α := (↑(h.U i) : Type u))
                            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                    (CC := carrier) (h.V i j).inclusion' :
                                  (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                                p.1 :
                              (↑(h.U i) : Type u))
                            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                    (CC := carrier) (h.V i k).inclusion' :
                                  (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                                p.2 :
                              (↑(h.U i) : Type u)) }) ↦
                    Subtype.mk (p :=
                      fun
                        (p :
                          (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j k)) : Type u) ×
                            (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u)) ↦
                      Eq (α := (↑(h.U j) : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (h.V j k).inclusion' :
                              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) → (↑(h.U j) : Type u))
                            p.1 :
                          (↑(h.U j) : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (h.V j i).inclusion' :
                              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) → (↑(h.U j) : Type u))
                            p.2 :
                          (↑(h.U j) : Type u)))
                      (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
                          (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                    (CC := carrier) (h.t i j) :
                                  (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
                                    (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
                                (↑x :
                                    (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u) ×
                                      (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)).1) :
                            (↑(h.U j) : Type u))
                          ⋯,
                        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) (h.t i j) :
                            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
                              (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
                          (↑x :
                              (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u) ×
                                (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)).1)
                      ⋯,
                  continuous_toFun := ⋯ :
                  C({ p :
                      (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
                        (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
                      Eq (α := (↑(h.U i) : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (h.V i j).inclusion' :
                              (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                            p.1 :
                          (↑(h.U i) : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (h.V i k).inclusion' :
                              (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                            p.2 :
                          (↑(h.U i) : Type u)) },
                    { p :
                      (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j k)) : Type u) ×
                        (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u) //
                      Eq (α := (↑(h.U j) : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (h.V j k).inclusion' :
                              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) → (↑(h.U j) : Type u))
                            p.1 :
                          (↑(h.U j) : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (h.V j i).inclusion' :
                              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) → (↑(h.U j) : Type u))
                            p.2 :
                          (↑(h.U j) : Type u)) }) } ≫
              ofHom
                  {
                    toFun :=
                      fun
                        (x :
                          { p :
                            (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j k)) : Type u) ×
                              (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u) //
                            Eq (α := (↑(h.U j) : Type u))
                              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                      (CC := carrier) (h.V j k).inclusion' :
                                    (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) → (↑(h.U j) : Type u))
                                  p.1 :
                                (↑(h.U j) : Type u))
                              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                      (CC := carrier) (h.V j i).inclusion' :
                                    (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) → (↑(h.U j) : Type u))
                                  p.2 :
                                (↑(h.U j) : Type u)) }) ↦
                      Subtype.mk (p :=
                        fun
                          (p :
                            (↑(Functor.obj (Opens.toTopCat (h.U k)) (h.V k i)) : Type u) ×
                              (↑(Functor.obj (Opens.toTopCat (h.U k)) (h.V k j)) : Type u)) ↦
                        Eq (α := (↑(h.U k) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V k i).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) → (↑(h.U k) : Type u))
                              p.1 :
                            (↑(h.U k) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V k j).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u)) → (↑(h.U k) : Type u))
                              p.2 :
                            (↑(h.U k) : Type u)))
                        (Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
                            (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                      (CC := carrier) (h.t j k) :
                                    (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                                      (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
                                  (↑x :
                                      (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u) ×
                                        (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)).1) :
                              (↑(h.U k) : Type u))
                            ⋯,
                          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (h.t j k) :
                              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                                (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
                            (↑x :
                                (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u) ×
                                  (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)).1)
                        ⋯,
                    continuous_toFun := ⋯ :
                    C({ p :
                        (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j k)) : Type u) ×
                          (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u) //
                        Eq (α := (↑(h.U j) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V j k).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) → (↑(h.U j) : Type u))
                              p.1 :
                            (↑(h.U j) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V j i).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) → (↑(h.U j) : Type u))
                              p.2 :
                            (↑(h.U j) : Type u)) },
                      { p :
                        (↑(Functor.obj (Opens.toTopCat (h.U k)) (h.V k i)) : Type u) ×
                          (↑(Functor.obj (Opens.toTopCat (h.U k)) (h.V k j)) : Type u) //
                        Eq (α := (↑(h.U k) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V k i).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) → (↑(h.U k) : Type u))
                              p.1 :
                            (↑(h.U k) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V k j).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u)) → (↑(h.U k) : Type u))
                              p.2 :
                            (↑(h.U k) : Type u)) }) } ≫
                ofHom
                  {
                    toFun :=
                      fun
                        (x :
                          { p :
                            (↑(Functor.obj (Opens.toTopCat (h.U k)) (h.V k i)) : Type u) ×
                              (↑(Functor.obj (Opens.toTopCat (h.U k)) (h.V k j)) : Type u) //
                            Eq (α := (↑(h.U k) : Type u))
                              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                      (CC := carrier) (h.V k i).inclusion' :
                                    (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) → (↑(h.U k) : Type u))
                                  p.1 :
                                (↑(h.U k) : Type u))
                              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                      (CC := carrier) (h.V k j).inclusion' :
                                    (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u)) → (↑(h.U k) : Type u))
                                  p.2 :
                                (↑(h.U k) : Type u)) }) ↦
                      Subtype.mk (p :=
                        fun
                          (p :
                            (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
                              (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u)) ↦
                        Eq (α := (↑(h.U i) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V i j).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                              p.1 :
                            (↑(h.U i) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V i k).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                              p.2 :
                            (↑(h.U i) : Type u)))
                        (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j)
                            (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                      (CC := carrier) (h.t k i) :
                                    (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) →
                                      (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u))
                                  (↑x :
                                      (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u) ×
                                        (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u)).1) :
                              (↑(h.U i) : Type u))
                            ⋯,
                          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (h.t k i) :
                              (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) →
                                (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u))
                            (↑x :
                                (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u) ×
                                  (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u)).1)
                        ⋯,
                    continuous_toFun := ⋯ :
                    C({ p :
                        (↑(Functor.obj (Opens.toTopCat (h.U k)) (h.V k i)) : Type u) ×
                          (↑(Functor.obj (Opens.toTopCat (h.U k)) (h.V k j)) : Type u) //
                        Eq (α := (↑(h.U k) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V k i).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) → (↑(h.U k) : Type u))
                              p.1 :
                            (↑(h.U k) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V k j).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u)) → (↑(h.U k) : Type u))
                              p.2 :
                            (↑(h.U k) : Type u)) },
                      { p :
                        (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
                          (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
                        Eq (α := (↑(h.U i) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V i j).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                              p.1 :
                            (↑(h.U i) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  carrier) (h.V i k).inclusion' :
                                (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                              p.2 :
                            (↑(h.U i) : Type u)) }) }) :
          (a :
              (↑(of
                    { p :
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u) ×
                        (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u) //
                      (ConcreteCategory.hom (h.V i j).inclusion' :
                            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                          p.1 =
                        (ConcreteCategory.hom (h.V i k).inclusion' :
                            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                          p.2 }) :
                Type u)) →
            (↑(of
                  { p :
                    (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u) ×
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u) //
                    (ConcreteCategory.hom (h.V i j).inclusion' :
                          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                        p.1 =
                      (ConcreteCategory.hom (h.V i k).inclusion' :
                          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                        p.2 }) :
              Type u))
        (Subtype.mk (p :=
          fun
            (p :
              (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
                (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u)) ↦
          Eq (α := (↑(h.U i) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.V i j).inclusion' :
                  (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                p.1 :
              (↑(h.U i) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.V i k).inclusion' :
                  (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                p.2 :
              (↑(h.U i) : Type u)))
          (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx,
            Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')
          ⋯) :
      (↑(of
            { p :
              (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
                (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
              Eq (α := (↑(h.U i) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (h.V i j).inclusion' :
                      (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                    p.1 :
                  (↑(h.U i) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (h.V i k).inclusion' :
                      (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                    p.2 :
                  (↑(h.U i) : Type u)) }) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (𝟙
              (of
                { p :
                  (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
                    (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
                  Eq (α := (↑(h.U i) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) (h.V i j).inclusion' :
                          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                        p.1 :
                      (↑(h.U i) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) (h.V i k).inclusion' :
                          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                        p.2 :
                      (↑(h.U i) : Type u)) })) :
          (a :
              (↑(of
                    { p :
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u) ×
                        (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u) //
                      (ConcreteCategory.hom (h.V i j).inclusion' :
                            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                          p.1 =
                        (ConcreteCategory.hom (h.V i k).inclusion' :
                            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                          p.2 }) :
                Type u)) →
            (↑(of
                  { p :
                    (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u) ×
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u) //
                    (ConcreteCategory.hom (h.V i j).inclusion' :
                          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                        p.1 =
                      (ConcreteCategory.hom (h.V i k).inclusion' :
                          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                        p.2 }) :
              Type u))
        (Subtype.mk (p :=
          fun
            (p :
              (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
                (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u)) ↦
          Eq (α := (↑(h.U i) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.V i j).inclusion' :
                  (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                p.1 :
              (↑(h.U i) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.V i k).inclusion' :
                  (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                p.2 :
              (↑(h.U i) : Type u)))
          (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx,
            Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')
          ⋯) :
      (↑(of
            { p :
              (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
                (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
              Eq (α := (↑(h.U i) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (h.V i j).inclusion' :
                      (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                    p.1 :
                  (↑(h.U i) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (h.V i k).inclusion' :
                      (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                    p.2 :
                  (↑(h.U i) : Type u)) }) :
        Type u))

Tactic:
dsimp only [Opens.coe_inclusion', hom_comp, hom_ofHom, ContinuousMap.comp_assoc,
      ContinuousMap.comp_apply, ContinuousMap.coe_mk, hom_id, ContinuousMap.id_apply]

Premises used: TopologicalSpace.Opens.coe_inclusion', TopCat.hom_ofHom, TopCat.hom_id, ContinuousMap.comp_apply, ContinuousMap.coe_mk, ContinuousMap.comp_assoc, ContinuousMap.id_apply, TopCat.hom_comp