∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  (Y : Action FintypeCat (CategoryTheory.Aut F)) (i : Y ⟶ (CategoryTheory.PreGaloisCategory.functorToAction F).obj X)
  [CategoryTheory.Mono i] [CategoryTheory.PreGaloisCategory.IsConnected Y],
  ∃ Z f u,
    CategoryTheory.PreGaloisCategory.IsConnected Z ∧
      CategoryTheory.Mono f ∧
        i = CategoryTheory.CategoryStruct.comp u.hom ((CategoryTheory.PreGaloisCategory.functorToAction F).map f)