-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
h : MkCore
i j k : h.J
⊢ (((((((pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
                  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)) }) }) ≫
                (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').inv) ≫
              (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').hom) ≫
            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)) }) }) ≫
          (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').inv) ≫
        (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').hom) ≫
      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)) }) } =
    𝟙 (pullback (h.V i j).inclusion' (h.V i k).inclusion') ≫
      (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom
have simp : (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
    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))
                  sorry,
                (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)
              sorry,
          continuous_toFun := sorry :
          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))
                    sorry,
                  (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)
                sorry,
            continuous_toFun := sorry :
            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))
                    sorry,
                  (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)
                sorry,
            continuous_toFun := sorry :
            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)) }) } =
  (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom
Tactic: simp only [Iso.inv_hom_id_assoc, Category.assoc, Category.id_comp]