-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Full (goal)
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)
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
    IsConnected.{u_1, v_1} Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f
have obtain : ∀ (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),
  ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
    IsConnected.{u_1, v_1} Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f
Tactic: obtain ⟨u, hu⟩ := connected_component_unique
    (forget₂ (Action FintypeCat (Aut F)) FintypeCat) (B := (functorToAction F).obj Z)
    y z i ((functorToAction F).map f) hz.symm