-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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) (Y :=
            coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap)
            (colimit.ι
              (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                D.diagram.sndSigmaMap)
              one) :
          (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) (Y :=
            coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap)
            (colimit.ι
              (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                D.diagram.sndSigmaMap)
              one) :
          (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)
⊢ 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))
have rw : Eq (α := (fun (X : Type u) ↦ X) (colimit diagram))
  (((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom
              (preservesColimitIso
                (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                  D.diagram.sndSigmaMap))) :
          TypeCat.Fun
            (Functor.obj
              (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              (colimit
                (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                  D.diagram.sndSigmaMap)))
            (colimit diagram)) :
        (a :
            (fun (X : Type u) ↦ X)
              ((forget TopCat).obj (colimit (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)))) →
          (fun (X : Type u) ↦ X) (colimit diagram))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (Y :=
                      colimit
                        (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                          D.diagram.sndSigmaMap))
                      (colimit.ι
                        (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                          D.diagram.sndSigmaMap)
                        one)) :
                  (a : (↑((parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap).obj one) : Type u)) →
                    (↑(colimit (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) : Type u))) :
            (a : (fun (X : Type u) ↦ X) (diagram.obj one)) →
              (fun (X : Type u) ↦ X)
                ((forget TopCat).obj (colimit (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap))))
          x :
        (fun (X : Type u) ↦ X)
          (Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
            (colimit
              (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                D.diagram.sndSigmaMap)))) :
    (fun (X : Type u) ↦ X) (colimit diagram))
  (((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y :=
              Functor.obj
                (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                (colimit
                  (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                    D.diagram.sndSigmaMap)))
              (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (Y :=
                      colimit
                        (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                          D.diagram.sndSigmaMap))
                      (colimit.ι
                        (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                          D.diagram.sndSigmaMap)
                        one)) :
                  (a : (↑((parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap).obj one) : Type u)) →
                    (↑(colimit (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) : Type u)))
              (Iso.hom
                (preservesColimitIso
                  (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
                  (parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                    D.diagram.sndSigmaMap)))) :
          TypeCat.Fun (diagram.obj one) (colimit diagram)) :
        (a : (fun (X : Type u) ↦ X) (diagram.obj one)) → (fun (X : Type u) ↦ X) (colimit diagram))
      y :
    (fun (X : Type u) ↦ X) (colimit diagram))
Tactic: rw [← ι_preservesColimitIso_hom, ConcreteCategory.forget_map_eq_ofHom, types_comp_apply]