-- 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 _ (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
                  (((evaluationEquivOfIsGalois F A.obj A.pt).symm : (a : (F.obj A.obj).obj) → Aut 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))) :
              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)
⊢ 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
                  (((evaluationEquivOfIsGalois F A.obj A.pt).symm : (a : (F.obj A.obj).obj) → Aut A.obj)
                    ((↑((endEquivSectionsFibers F :
                              (a : End F) → (↑(incl F ⋙ F ⋙ FintypeCat.incl).sections : Type (max u₁ u₂)))
                            f) :
                        (j : PointedGaloisObject F) → (F.obj j.obj).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:
simp only [endEquivSectionsFibers_π]

Premises used: CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π