-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.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))
            _ _ _ (F.map f ≫ (gapp Y).hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.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))
            _ _ _ ((gapp X).hom ≫ F.map f) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
have 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)
  ((@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: dsimp [gapp, e]