-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X_1 : C
inst_3 : IsConnected.{u₁, u₂} X_1
x_1 y : (F.obj X_1).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
e : (Y : C) → Equiv.{u₂ + 1, w + 1} (F'.obj Y).obj (F.obj Y).obj := fun (Y : C) ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X_1).obj := ((e X_1).symm : (a : (F.obj X_1).obj) → (F'.obj X_1).obj) x_1
hx' : x' = ((e X_1).symm : (a : (F.obj X_1).obj) → (F'.obj X_1).obj) x_1
y' : (F'.obj X_1).obj := ((e X_1).symm : (a : (F.obj X_1).obj) → (F'.obj X_1).obj) y
hy' : y' = ((e X_1).symm : (a : (F.obj X_1).obj) → (F'.obj X_1).obj) y
g' : Aut F'
hg' :
  (@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'.hom.app X_1) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F'.obj X_1)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F'.obj X_1))
      x' =
    y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun (Y : C) ↦
    (FintypeCat.equivEquivIso : (a : (F.obj Y).obj ≃ (F.obj Y).obj) → F.obj Y ≅ F.obj Y)
      ((e Y).symm.trans
        (Equiv.trans
          ((Equiv.symm FintypeCat.equivEquivIso : (a : F'.obj Y ≅ F'.obj Y) → (F'.obj Y).obj ≃ (F'.obj Y).obj)
            (Iso.app g' Y))
          (e Y)))
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
h :
  Eq.{w + 1} (α := (F.obj Y).obj)
    (((F.obj Y).uSwitchEquiv : (a : (F'.obj Y).obj) → (F.obj Y).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'.hom.app Y) :
            (a : (F'.obj Y).obj) → (F'.obj Y).obj)
          ((Equiv.symm (F.obj Y).uSwitchEquiv : (a : (F.obj Y).obj) → (F'.obj Y).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 f) :
                  (a : (F.obj X).obj) → (F.obj Y).obj)
                x) :
            (F'.obj Y).obj)) :
      (F.obj Y).obj)
    (((F.obj Y).uSwitchEquiv : (a : (FintypeCat.uSwitch.obj (F.obj Y)).obj) → (F.obj Y).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))
              _ _ _ (FintypeCat.uSwitch.map (F.map f)) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (FintypeCat.uSwitch.obj (F.obj X))) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (FintypeCat.uSwitch.obj (F.obj Y)))
          ((@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'.hom.app X) :
                (a : (F'.obj X).obj) → (F'.obj X).obj)
              ((Equiv.symm (F.obj X).uSwitchEquiv : (a : (F.obj X).obj) → (F'.obj X).obj) x : (F'.obj X).obj) :
            (F'.obj X).obj)) :
      (F.obj Y).obj)
⊢ Eq.{w + 1} (α := (F.obj Y).obj)
    (((F.obj Y).uSwitchEquiv : (a : (F'.obj Y).obj) → (F.obj Y).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'.hom.app Y) :
            (a : (F'.obj Y).obj) → (F'.obj Y).obj)
          ((Equiv.symm (F.obj Y).uSwitchEquiv : (a : (F.obj Y).obj) → (F'.obj Y).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 f) :
                  (a : (F.obj X).obj) → (F.obj Y).obj)
                x) :
            (F'.obj Y).obj)) :
      (F.obj Y).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 f) :
          (a : (F.obj X).obj) → (F.obj Y).obj)
        (((F.obj X).uSwitchEquiv : (a : (F'.obj X).obj) → (F.obj X).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'.hom.app X) :
                (a : (F'.obj X).obj) → (F'.obj X).obj)
              ((Equiv.symm (F.obj X).uSwitchEquiv : (a : (F.obj X).obj) → (F'.obj X).obj) x : (F'.obj X).obj)) :
          (F.obj X).obj) :
      (F.obj Y).obj)

Tactic:
erw [FintypeCat.uSwitchEquiv_naturality (F.map f)]

Premises used: FintypeCat.uSwitchEquiv_naturality, CategoryTheory.Functor.map