-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
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
simp :
  Eq (α := (F.obj A.obj).obj)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              ((FullyFaithful.homEquiv ((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C) :
                  (a : F ⟶ F) → F ⋙ FintypeCat.incl ⟶ F ⋙ FintypeCat.incl)
                f)
              A.obj) :
          (a : (F.obj A.obj).obj) → (F.obj A.obj).obj)
        A.pt :
      (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)
⊢ 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:
simp