-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
w :
  ∀ (x : (↑(h.U i) : Type u)) (hx : x ∈ h.V i j) (hx' : x ∈ h.V i k),
    Eq (α :=
      (↑(Functor.obj (C := Opens (↑(h.U (j, i).1) : Type u)) (Opens.toTopCat (h.U (j, i).1)) (h.V (j, i).1 (j, i).2)) :
        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)) }) } ≫
                pullbackSnd (h.V j k).inclusion' (h.V j i).inclusion') :
            (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)) →
              (↑((Opens.toTopCat (h.U (j, i).1)).obj (h.V (j, i).1 (j, i).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')
            ⋯) :
        (↑(Functor.obj (C := Opens (↑(h.U (j, i).1) : Type u)) (Opens.toTopCat (h.U (j, i).1))
              (h.V (j, i).1 (j, i).2)) :
          Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (pullbackFst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j) :
            (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)) →
              (↑((Opens.toTopCat (h.U (j, i).1)).obj (h.V (j, i).1 (j, i).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')
            ⋯) :
        (↑(Functor.obj (C := Opens (↑(h.U (j, i).1) : Type u)) (Opens.toTopCat (h.U (j, i).1))
              (h.V (j, i).1 (j, i).2)) :
          Type u))
⊢ 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)) }) } ≫
      pullbackSnd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullbackFst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j

Tactic:
ext ⟨⟨⟨x, hx⟩, ⟨x', hx'⟩⟩, rfl : x = x'⟩

Premises used: rfl