-- 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 g : 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.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))
        ((@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))
                _ _ _ (g.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)) :
      (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.map
                  (Iso.hom
                    ((AutGalois.π F A : (a : AutGalois F) → Aut A.obj)
                      ((endEquivAutGalois F : (a : End F) → AutGalois F) g))) :
              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))
⊢ 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.app A.obj : F.obj A.obj ⟶ F.obj A.obj) :
          (a : (F.obj A.obj).obj) → (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))
                _ _ _ (g.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).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
                  ((AutGalois.π F A : (a : AutGalois F) → Aut A.obj)
                    ((endEquivAutGalois F : (a : End F) → AutGalois F) g))) :
              F.obj A.obj ⟶ F.obj A.obj) :
          (a : (F.obj A.obj).obj) → (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) :
      (F.obj A.obj).obj)

Tactic:
change f.app A (g.app A A.pt) =
    (f.app A ≫ F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt

Premises used: CategoryTheory.PreGaloisCategory.PointedGaloisObject.pt, CategoryTheory.PreGaloisCategory.AutGalois.π, CategoryTheory.ConcreteCategory.hom, CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.PreGaloisCategory.endEquivAutGalois, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.NatTrans.app