-- Lean 4 proof step from Mathlib.Topology.Gluing (hypothesis)
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))
⊢ 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
have 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)))))
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 :
      _)