-- 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) (X :=
            ∐ D.diagram.right) (Y :=
            coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap)
            (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
          (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) (X :=
            ∐ D.diagram.right) (Y :=
            coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap)
            (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
          (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)
this_1 :
  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))
this :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Cocone.pt (F :=
        parallelPair (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right))
        (ColimitCocone.cocone
          (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
            (diagram.map WalkingParallelPairHom.right)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := colimit diagram) (colimit.ι diagram one)
              (CategoryStruct.comp (Y :=
                Functor.obj colim
                  (parallelPair (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right)))
                (CategoryTheory.Functor.map colim (diagramIsoParallelPair diagram).hom)
                (Iso.hom
                  (colimit.isoColimitCocone
                    (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                      (diagram.map WalkingParallelPairHom.right)))))) :
          (a : (fun (X : Type u) ↦ X) (diagram.obj one)) →
            (fun (X : Type u) ↦ X)
              (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                    (diagram.map WalkingParallelPairHom.right)).cocone.pt)
        x :
      (fun (X : Type u) ↦ X)
        (Cocone.pt (F :=
          parallelPair (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right))
          (ColimitCocone.cocone
            (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
              (diagram.map WalkingParallelPairHom.right)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := colimit diagram) (colimit.ι diagram one)
              (CategoryStruct.comp (Y :=
                Functor.obj colim
                  (parallelPair (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right)))
                (CategoryTheory.Functor.map colim (diagramIsoParallelPair diagram).hom)
                (Iso.hom
                  (colimit.isoColimitCocone
                    (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                      (diagram.map WalkingParallelPairHom.right)))))) :
          (a : (fun (X : Type u) ↦ X) (diagram.obj one)) →
            (fun (X : Type u) ↦ X)
              (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                    (diagram.map WalkingParallelPairHom.right)).cocone.pt)
        y :
      (fun (X : Type u) ↦ X)
        (Cocone.pt (F :=
          parallelPair (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right))
          (ColimitCocone.cocone
            (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
              (diagram.map WalkingParallelPairHom.right)))))
⊢ Eq (α :=
    Cocone.pt (F := parallelPair (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right))
      (ColimitCocone.cocone
        (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
          (diagram.map WalkingParallelPairHom.right))))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app
                (Cocone.ι
                  (ColimitCocone.cocone
                    (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                      (diagram.map WalkingParallelPairHom.right))))
                one) :
            TypeCat.Fun (diagram.obj one)
              (Cocone.pt (F :=
                parallelPair (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right))
                (ColimitCocone.cocone
                  (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                    (diagram.map WalkingParallelPairHom.right))))) :
          (a : diagram.obj one) →
            (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                  (diagram.map WalkingParallelPairHom.right)).cocone.pt)
        x :
      Cocone.pt (F := parallelPair (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right))
        (ColimitCocone.cocone
          (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
            (diagram.map WalkingParallelPairHom.right))))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app
                (Cocone.ι
                  (ColimitCocone.cocone
                    (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                      (diagram.map WalkingParallelPairHom.right))))
                one) :
            TypeCat.Fun (diagram.obj one)
              (Cocone.pt (F :=
                parallelPair (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right))
                (ColimitCocone.cocone
                  (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                    (diagram.map WalkingParallelPairHom.right))))) :
          (a : diagram.obj one) →
            (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                  (diagram.map WalkingParallelPairHom.right)).cocone.pt)
        y :
      Cocone.pt (F := parallelPair (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right))
        (ColimitCocone.cocone
          (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
            (diagram.map WalkingParallelPairHom.right))))

Tactic:
simp only [eqToHom_refl, colimit.ι_map_assoc, diagramIsoParallelPair_hom_app,
    colimit.isoColimitCocone_ι_hom, Category.id_comp] at this

Premises used: CategoryTheory.Limits.diagramIsoParallelPair_hom_app, CategoryTheory.eqToHom_refl, CategoryTheory.Limits.colimit.ι_map_assoc, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom, CategoryTheory.Category.id_comp