-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : C ⥤ FintypeCat
inst_2 : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ Eq (α := (F.obj A.obj).obj)
    (ULift.down.{u₁, u₂}
        {
          down :=
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app
                    (CategoryStruct.comp (Y := Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (cocone F))
                      (Iso.hom
                          (colimit.isoColimitCocone
                            { cocone := cocone F, isColimit := isColimit F :
                              ColimitCocone (J := (PointedGaloisObject F)ᵒᵖ) (Functor.op (incl F) ⋙ coyoneda) }) :
                        colimit (J := (PointedGaloisObject F)ᵒᵖ) (Functor.op (incl F) ⋙ coyoneda) ⟶
                          Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (cocone F))
                      ((FullyFaithful.homEquiv ((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C) :
                          (a : End F) → End (F ⋙ FintypeCat.incl))
                        f))
                    (Functor.obj (incl F) A)) :
                (a : (colimit ((incl F).op ⋙ coyoneda)).obj ((incl F).obj A)) →
                  (F ⋙ FintypeCat.incl).obj ((incl F).obj A))
              ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                      (NatTrans.app (colimit.ι (Functor.op (incl F) ⋙ coyoneda) (Opposite.op A))
                        (Functor.obj (incl F) A)) :
                    (a : (incl F).obj A ⟶ (incl F).obj A) → (colimit ((incl F).op ⋙ coyoneda)).obj ((incl F).obj A))
                  (𝟙 (Functor.obj (incl F) A)) :
                (colimit (J := (PointedGaloisObject F)ᵒᵖ) (Functor.op (incl F) ⋙ coyoneda)).obj
                  (Functor.obj (incl F) A)) } :
      (F.obj A.obj).obj)
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (f.app A.obj : F.obj A.obj ⟶ F.obj A.obj) :
          (a : (F.obj A.obj).obj) → (F.obj A.obj).obj)
        A.pt :
      (F.obj A.obj).obj)
have change : Eq (α :=
  (fun (X : Type u₂) ↦ X)
    ((Functor.obj (Functor.obj (whiskeringRight C FintypeCat (Type u₂)) FintypeCat.incl) F).obj A.obj))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((FullyFaithful.homEquiv ((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C) :
                (a : F ⟶ F) →
                  ((whiskeringRight C FintypeCat (Type u₂)).obj FintypeCat.incl).obj F ⟶
                    ((whiskeringRight C FintypeCat (Type u₂)).obj FintypeCat.incl).obj F)
              f)
            A.obj) :
        (a :
            (fun (X : Type u₂) ↦ X)
              ((((whiskeringRight C FintypeCat (Type u₂)).obj FintypeCat.incl).obj F).obj A.obj)) →
          (fun (X : Type u₂) ↦ X) ((((whiskeringRight C FintypeCat (Type u₂)).obj FintypeCat.incl).obj F).obj A.obj))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (CategoryStruct.comp (Y := colimit (J := (PointedGaloisObject F)ᵒᵖ) (Functor.op (incl F) ⋙ coyoneda))
                  (colimit.ι (Functor.op (incl F) ⋙ coyoneda) (Opposite.op A))
                  (Iso.hom
                    (colimit.isoColimitCocone
                      { cocone := cocone F, isColimit := isColimit F :
                        ColimitCocone (J := (PointedGaloisObject F)ᵒᵖ) (Functor.op (incl F) ⋙ coyoneda) })))
                A.obj) :
            (a : (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda).obj (Opposite.op A)).obj A.obj)) →
              (fun (X : Type u₂) ↦ X) ({ cocone := cocone F, isColimit := isColimit F }.cocone.pt.obj A.obj))
          (𝟙 (Functor.obj (incl F) A)) :
        (fun (X : Type u₂) ↦ X)
          ((Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ)
                (ColimitCocone.cocone
                  { cocone := cocone F, isColimit := isColimit F :
                    ColimitCocone (J := (PointedGaloisObject F)ᵒᵖ) (Functor.op (incl F) ⋙ coyoneda) })).obj
            A.obj)) :
    (fun (X : Type u₂) ↦ X)
      ((Functor.obj (Functor.obj (whiskeringRight C FintypeCat (Type u₂)) FintypeCat.incl) F).obj A.obj))
  ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (f.app A.obj : F.obj A.obj ⟶ F.obj A.obj) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj))
      A.pt :
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj))
Tactic: change (((FullyFaithful.whiskeringRight (FullyFaithful.ofFullyFaithful
      FintypeCat.incl) C).homEquiv) f).app A
    (((colimit.ι _ _) ≫ (colimit.isoColimitCocone ⟨cocone F, isColimit F⟩).hom).app
      A _) = f.app A A.pt