-- 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
x : AutGalois F
A : C
inst_3 : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
rw :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    ((@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 { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F } :
                      (a_1 : AutGalois F) → Aut { obj := A, pt := a, isGalois := ⋯ }.obj)
                    (MulOpposite.unop { unop' := x }))) :
              F.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.obj ⟶
                F.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.obj) :
          (a_1 :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (F.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.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 { obj := A, pt := a, isGalois := ⋯ } :
                      (a_1 : AutGalois F) → Aut { obj := A, pt := a, isGalois := ⋯ }.obj)
                    x)) :
              F.obj (PointedGaloisObject.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }) ⟶
                F.obj (PointedGaloisObject.obj { obj := A, pt := a, isGalois := ⋯ })) :
          (a_1 :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (F.obj (PointedGaloisObject.obj { obj := A, pt := a, isGalois := ⋯ })))
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    ((@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))
            _ _ _
            (NatTrans.app
                (Iso.hom ((MulEquiv.symm (autMulEquivAutGalois F) : (a : (AutGalois F)ᵐᵒᵖ) → Aut F) { unop' := x })) A :
              F.obj A ⟶ F.obj A) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    ((@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 { obj := A, pt := a, isGalois := ⋯ } :
                      (a_1 : AutGalois F) → Aut { obj := A, pt := a, isGalois := ⋯ }.obj)
                    x)) :
              F.obj (PointedGaloisObject.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }) ⟶
                F.obj (PointedGaloisObject.obj { obj := A, pt := a, isGalois := ⋯ })) :
          (a_1 :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (F.obj (PointedGaloisObject.obj { obj := A, pt := a, isGalois := ⋯ })))

Tactic:
rw [← autMulEquivAutGalois_π, MulEquiv.apply_symm_apply]

Premises used: CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π, MulEquiv.apply_symm_apply