-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
a : (↑(D.U i) : Type u)
j : D.J
b : (↑(D.U j) : Type u)
k : D.J
c : (↑(D.U k) : Type u)
x :
  (↑(D.V
        (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a),
          Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
    Type u)
e₁ :
  Eq (α :=
    (↑(D.U
          (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            D.V
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a),
                Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b)))
            (D.f
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
          (a_1 : (↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst)) : Type u)) → (↑(D.U ⟨i, a⟩.fst) : Type u))
        x :
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))) :
        Type u))
    (Sigma.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a) :
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))) :
        Type u))
e₂ :
  Eq (α :=
    (↑(D.U
          (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            D.V
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b),
                Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a)))
            (D.f
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))) :
          (a : (↑(D.V (⟨j, b⟩.fst, ⟨i, a⟩.fst)) : Type u)) → (↑(D.U ⟨j, b⟩.fst) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                D.V
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a),
                    Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b)))
                (D.t
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
              (a_1 : (↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst)) : Type u)) → (↑(D.V (⟨j, b⟩.fst, ⟨i, a⟩.fst)) : Type u))
            x :
          (↑(D.V
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b),
                  Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))) :
            Type u)) :
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
        Type u))
    (Sigma.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b) :
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
        Type u))
y :
  (↑(D.V
        (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b),
          Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
    Type u)
e₃ :
  Eq (α :=
    (↑(D.U
          (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            D.V
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b),
                Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c)))
            (D.f
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
          (a : (↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst)) : Type u)) → (↑(D.U ⟨j, b⟩.fst) : Type u))
        y :
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
        Type u))
    (Sigma.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b) :
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
        Type u))
e₄ :
  Eq (α :=
    (↑(D.U
          (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            D.V
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c),
                Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b)))
            (D.f
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
          (a : (↑(D.V (⟨k, c⟩.fst, ⟨j, b⟩.fst)) : Type u)) → (↑(D.U ⟨k, c⟩.fst) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                D.V
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b),
                    Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c)))
                (D.t
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
              (a : (↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst)) : Type u)) → (↑(D.V (⟨k, c⟩.fst, ⟨j, b⟩.fst)) : Type u))
            y :
          (↑(D.V
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c),
                  Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
            Type u)) :
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
        Type u))
    (Sigma.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c) :
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
        Type u))
z : (↑(pullback (D.f j i) (D.f j k)) : Type u)
eq₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.t j i) :
        (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback (D.f j i) (D.f j k)) (pullback.fst (D.f j i) (D.f j k)) :
            (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, i)) : Type u))
          z :
        (↑(D.V (j, i)) : Type u)) =
    x
eq₂ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback (D.f j i) (D.f j k)) (pullback.snd (D.f j i) (D.f j k)) :
        (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, k)) : Type u))
      z =
    y
h :
  Eq (α :=
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              D.V
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a),
                  Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c)))
              (D.f
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
            (a_1 : (↑(D.V (⟨i, a⟩.fst, ⟨k, c⟩.fst)) : Type u)) → (↑(D.U ⟨i, a⟩.fst) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  pullback (D.f i k) (D.f i j)) (pullback.fst (D.f i k) (D.f i j)) :
                (a : (↑(pullback (D.f i k) (D.f i j)) : Type u)) → (↑(D.V (i, k)) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (D.t' j i k) :
                    (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(pullback (D.f i k) (D.f i j)) : Type u))
                  z :
                (↑(pullback (D.f i k) (D.f i j)) : Type u)) :
            (↑(D.V (i, k)) : Type u)) :
        (↑(D.U
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))) :
          Type u))
      (Sigma.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a) :
        (↑(D.U
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))) :
          Type u)) ∧
    Eq (α :=
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              D.V
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c),
                  Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a)))
              (D.f
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))) :
            (a : (↑(D.V (⟨k, c⟩.fst, ⟨i, a⟩.fst)) : Type u)) → (↑(D.U ⟨k, c⟩.fst) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  D.V
                    (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a),
                      Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c)))
                  (D.t
                    (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))
                    (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
                (a_1 : (↑(D.V (⟨i, a⟩.fst, ⟨k, c⟩.fst)) : Type u)) → (↑(D.V (⟨k, c⟩.fst, ⟨i, a⟩.fst)) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (X := pullback (D.f i k) (D.f i j)) (pullback.fst (D.f i k) (D.f i j)) :
                    (a : (↑(pullback (D.f i k) (D.f i j)) : Type u)) → (↑(D.V (i, k)) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) (D.t' j i k) :
                        (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(pullback (D.f i k) (D.f i j)) : Type u))
                      z :
                    (↑(pullback (D.f i k) (D.f i j)) : Type u)) :
                (↑(D.V (i, k)) : Type u)) :
            (↑(D.V
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c),
                    Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a))) :
              Type u)) :
        (↑(D.U
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
          Type u))
      (Sigma.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c) :
        (↑(D.U
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
          Type u))
⊢ D.Rel (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i a)
    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c)

Tactic:
use (pullback.fst _ _ : _ ⟶ D.V (i, k)) (D.t' _ _ _ z)

Premises used: CategoryTheory.ConcreteCategory.hom, TopCat.GlueData.toGlueData, CategoryTheory.GlueData.t', CategoryTheory.Limits.pullback.fst, DFunLike.coe