-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
inst_4 : IsConnected Y
y :
  (obj
      (forget₂ (Action FintypeCat (Aut F)) (FC :=
        Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
        (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
        fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
      Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@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 : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@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))
            _ _ _ i.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
        y :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
hc : IsConnected.{u_1, v_1} Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu :
  (@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))
          _ _ _
          (map
              (forget₂ (Action FintypeCat (Aut F)) (FC :=
                Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
              u.hom :
            obj
                (forget₂ (Action FintypeCat (Aut F)) (FC :=
                  Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                    TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                  (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                  fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                  fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                Y ⟶
              obj
                (forget₂ (Action FintypeCat (Aut F)) (FC :=
                  Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                    TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                  (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                  fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                  fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                ((functorToAction F).obj Z)) :
        (a :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj ((functorToAction F).obj Z)))
      y =
    z
a :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
    ((@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))
            _ _ _ i.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
        y :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
    ((@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 : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
⊢ Eq.{u + 1} (α :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
      (obj
        (forget₂ (Action FintypeCat (Aut F)) (FC :=
          Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
          (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
          fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
          fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
        ((functorToAction F).obj X)))
    ((fun (f : Y ⟶ (functorToAction F).obj X) ↦
        ((@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))
                _ _ _
                (map
                    (forget₂ (Action FintypeCat (Aut F)) (FC :=
                      Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                        TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                      (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                      fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                    f :
                  obj
                      (forget₂ (Action FintypeCat (Aut F)) (FC :=
                        Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                          TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                        (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                        fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                      Y ⟶
                    obj
                      (forget₂ (Action FintypeCat (Aut F)) (FC :=
                        Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                          TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                        (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                        fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                      ((functorToAction F).obj X)) :
              (a :
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                    ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                  ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj ((functorToAction F).obj X)))
            y :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (obj
              (forget₂ (Action FintypeCat (Aut F)) (FC :=
                Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
              ((functorToAction F).obj X))))
      i)
    ((fun (f : Y ⟶ (functorToAction F).obj X) ↦
        ((@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))
                _ _ _
                (map
                    (forget₂ (Action FintypeCat (Aut F)) (FC :=
                      Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                        TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                      (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                      fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                    f :
                  obj
                      (forget₂ (Action FintypeCat (Aut F)) (FC :=
                        Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                          TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                        (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                        fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                      Y ⟶
                    obj
                      (forget₂ (Action FintypeCat (Aut F)) (FC :=
                        Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                          TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                        (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                        fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                      ((functorToAction F).obj X)) :
              (a :
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                    ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                  ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj ((functorToAction F).obj X)))
            y :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (obj
              (forget₂ (Action FintypeCat (Aut F)) (FC :=
                Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
                fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
                fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
              ((functorToAction F).obj X))))
      (u.hom ≫ (functorToAction F).map f))

Tactic:
suffices h : i.hom y = F.map f z by simpa [hu]