-- 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
change :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (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.map
                (Iso.hom
                  ((↑((ConcreteCategory.hom (FC := TypeCat.Fun)
                              (map (sectionsFunctor (PointedGaloisObject F)) (Iso.inv (autIsoFibers F))) :
                            (a :
                                (fun (X : Type (max u₁ u₂)) ↦ X)
                                  ((sectionsFunctor (PointedGaloisObject F)).obj (incl F ⋙ F ⋙ FintypeCat.incl))) →
                              (fun (X : Type (max u₁ u₂)) ↦ X)
                                ((sectionsFunctor (PointedGaloisObject F)).obj (autGaloisSystem F ⋙ forget GrpCat)))
                          ((endEquivSectionsFibers F :
                              (a : End F) → (↑(incl F ⋙ F ⋙ FintypeCat.incl).sections : Type (max u₁ u₂)))
                            f)) :
                      (j : PointedGaloisObject F) → (autGaloisSystem F ⋙ forget GrpCat).obj j)
                    A)) :
              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))
    ((@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 (α := (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.map
                (Iso.hom
                  ((↑(((Iso.toEquiv (Iso.symm (mapIso (sectionsFunctor (PointedGaloisObject F)) (autIsoFibers F))) :
                              (↑(sections (incl F ⋙ F ⋙ FintypeCat.incl) :
                                      Set
                                        ((j : PointedGaloisObject F) → Functor.obj (incl F ⋙ F ⋙ FintypeCat.incl) j)) :
                                  Type (max u₁ u₂)) ≃
                                (↑(sections
                                        (autGaloisSystem F ⋙
                                          forget GrpCat (FC := fun (x1 x2 : GrpCat.{u₂}) ↦
                                            (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier)) :
                                      Set
                                        ((j : PointedGaloisObject F) →
                                          Functor.obj
                                            (autGaloisSystem F ⋙
                                              forget GrpCat (FC := fun (x1 x2 : GrpCat.{u₂}) ↦
                                                (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier))
                                            j)) :
                                  Type (max u₁ u₂))) :
                            (a : (↑(incl F ⋙ F ⋙ FintypeCat.incl).sections : Type (max u₁ u₂))) → AutGalois F)
                          ((endEquivSectionsFibers F :
                              (a : End F) → (↑(incl F ⋙ F ⋙ FintypeCat.incl).sections : Type (max u₁ u₂)))
                            f)) :
                      (j : PointedGaloisObject F) → Aut j.obj)
                    A)) :
              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)
    ((@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)

Tactic:
change F.map ((((sectionsFunctor _).map (autIsoFibers F).inv) _).val A).hom A.pt = _

Premises used: CategoryTheory.PreGaloisCategory.PointedGaloisObject.pt, CategoryTheory.ConcreteCategory.hom, CategoryTheory.PreGaloisCategory.autIsoFibers, CategoryTheory.Functor.map, Subtype.val, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.Functor.sectionsFunctor