-- 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 (α :=
    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))))
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel (α := (↑(∐ D.diagram.left) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap) :
        (a : (↑(∐ D.diagram.left) : Type u)) → (↑(∐ D.diagram.right) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.sndSigmaMap) :
        (a : (↑(∐ D.diagram.left) : Type u)) → (↑(∐ D.diagram.right) : Type u)))
    x y

Tactic:
exact Quot.eq.1 this

Premises used: Iff.mp, Quot.eq