-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
x y : (↑(∐ D.U) : Type u)
h :
  Eq (α :=
    (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap)
            (colimit.ι
              (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                D.diagram.sndSigmaMap)
              one) :
          (a : (↑(∐ D.diagram.right) : Type u)) → (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u))
        x :
      (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap)
            (colimit.ι
              (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                D.diagram.sndSigmaMap)
              one) :
          (a : (↑(∐ D.diagram.right) : Type u)) → (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u))
        y :
      (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
        Type u))
diagram : WalkingParallelPair ⥤ Type u :=
  parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙
    forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
rw :
  Eq (α := (fun (X : Type u) ↦ X) (colimit diagram))
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Iso.hom
                (preservesColimitIso
                  (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                  (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                    D.diagram.sndSigmaMap))) :
            TypeCat.Fun
              (Functor.obj
                (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                (colimit
                  (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                    D.diagram.sndSigmaMap)))
              (colimit diagram)) :
          (a :
              (fun (X : Type u) ↦ X)
                ((forget TopCat).obj (colimit (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)))) →
            (fun (X : Type u) ↦ X) (colimit diagram))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) (Y :=
                        colimit
                          (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                            D.diagram.sndSigmaMap))
                        (colimit.ι
                          (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                            D.diagram.sndSigmaMap)
                          one)) :
                    (a : (↑((parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap).obj one) : Type u)) →
                      (↑(colimit (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) : Type u))) :
              (a : (fun (X : Type u) ↦ X) (diagram.obj one)) →
                (fun (X : Type u) ↦ X)
                  ((forget TopCat).obj (colimit (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap))))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj
              (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              (colimit
                (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                  D.diagram.sndSigmaMap)))) :
      (fun (X : Type u) ↦ X) (colimit diagram))
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y :=
                Functor.obj
                  (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                  (colimit
                    (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                      D.diagram.sndSigmaMap)))
                (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) (Y :=
                        colimit
                          (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                            D.diagram.sndSigmaMap))
                        (colimit.ι
                          (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                            D.diagram.sndSigmaMap)
                          one)) :
                    (a : (↑((parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap).obj one) : Type u)) →
                      (↑(colimit (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) : Type u)))
                (Iso.hom
                  (preservesColimitIso
                    (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                    (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                      D.diagram.sndSigmaMap)))) :
            TypeCat.Fun (diagram.obj one) (colimit diagram)) :
          (a : (fun (X : Type u) ↦ X) (diagram.obj one)) → (fun (X : Type u) ↦ X) (colimit diagram))
        y :
      (fun (X : Type u) ↦ X) (colimit diagram))
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit diagram))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι diagram one) :
          (a : (fun (X : Type u) ↦ X) (diagram.obj one)) → (fun (X : Type u) ↦ X) (colimit diagram))
        x :
      (fun (X : Type u) ↦ X) (colimit diagram))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι diagram one) :
          (a : (fun (X : Type u) ↦ X) (diagram.obj one)) → (fun (X : Type u) ↦ X) (colimit diagram))
        y :
      (fun (X : Type u) ↦ X) (colimit diagram))

Tactic:
rw [← ι_preservesColimitIso_hom, ConcreteCategory.forget_map_eq_ofHom, types_comp_apply]

Premises used: CategoryTheory.ConcreteCategory.forget_map_eq_ofHom, CategoryTheory.ι_preservesColimitIso_hom, CategoryTheory.types_comp_apply