-- 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) :=
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
        (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv :
      (a :
          (↑(of
                { p : (↑(D.V (j, i)) : Type u) × (↑(D.V (j, k)) : Type u) //
                  (ConcreteCategory.hom (D.f j i) : (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u)) p.1 =
                    (ConcreteCategory.hom (D.f j k) : (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u)) p.2 }) :
            Type u)) →
        (↑(pullback (D.f j i) (D.f j k)) : Type u))
    (Subtype.mk (p := fun (p : (↑(D.V (j, i)) : Type u) × (↑(D.V (j, k)) : Type u)) ↦
        Eq (α := (↑(D.U j) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (D.f j i) :
                (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
              p.1 :
            (↑(D.U j) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (D.f j k) :
                (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
              p.2 :
            (↑(D.U j) : 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,
          y)
        ⋯ :
      { p : (↑(D.V (j, i)) : Type u) × (↑(D.V (j, k)) : Type u) //
        Eq (α := (↑(D.U j) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (D.f j i) :
                (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
              p.1 :
            (↑(D.U j) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (D.f j k) :
                (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
              p.2 :
            (↑(D.U j) : Type u)) })
rw :
  (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))
      ((↑(Subtype.mk (p := fun (p : (↑(D.V (j, i)) : Type u) × (↑(D.V (j, k)) : Type u)) ↦
                Eq (α := (↑(D.U j) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) (D.f j i) :
                        (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
                      p.1 :
                    (↑(D.U j) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) (D.f j k) :
                        (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
                      p.2 :
                    (↑(D.U j) : Type u)))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (D.t i j) :
                      (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
                    x,
                  y)
                ⋯) :
            (↑(D.V (j, i)) : Type u) × (↑(D.V (j, k)) : Type u)).1 :
        (↑(D.V (j, i)) : Type u)) =
    x
rw₁ rw₂ : x = x
⊢ (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))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv :
                (a :
                    { p : (↑(D.V (j, i)) : Type u) × (↑(D.V (j, k)) : Type u) //
                      (ConcreteCategory.hom (D.f j i) : (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u)) p.1 =
                        (ConcreteCategory.hom (D.f j k) : (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u)) p.2 }) →
                  (↑(pullback (D.f j i) (D.f j k)) : Type u))
              (Subtype.mk (p := fun (p : (↑(D.V (j, i)) : Type u) × (↑(D.V (j, k)) : Type u)) ↦
                  Eq (α := (↑(D.U j) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) (D.f j i) :
                          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
                        p.1 :
                      (↑(D.U j) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) (D.f j k) :
                          (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
                        p.2 :
                      (↑(D.U j) : Type u)))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) (D.t i j) :
                        (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
                      x,
                    y)
                  ⋯ :
                { p : (↑(D.V (j, i)) : Type u) × (↑(D.V (j, k)) : Type u) //
                  Eq (α := (↑(D.U j) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) (D.f j i) :
                          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
                        p.1 :
                      (↑(D.U j) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) (D.f j k) :
                          (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
                        p.2 :
                      (↑(D.U j) : Type u)) }) :
            (↑(pullback (D.f j i) (D.f j k)) : Type u)) :
        (↑(D.V (j, i)) : Type u)) =
    x

Tactic:
rw [pullbackIsoProdSubtype_inv_fst_apply, D.t_inv_apply]

Premises used: TopCat.GlueData.toGlueData, CategoryTheory.GlueData.t_inv_apply, TopCat.pullbackIsoProdSubtype_inv_fst_apply