-- 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_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)))))
⊢ 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 (α :=
  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
Cleared hypotheses: this