-- 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 :
  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))
⊢ 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)))))

Tactic:
have :
    (colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ =
      (colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ :=
    (congr_arg
        (colim.map (diagramIsoParallelPair diagram).hom ≫
          (colimit.isoColimitCocone (Types.coequalizerColimit _ _)).hom)
        this :
      _)