{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {F : CategoryTheory.Functor C FintypeCat} →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          (X : C) →
            [CategoryTheory.PreGaloisCategory.IsConnected X] →
              (x : (F.obj X).carrier) →
                (CategoryTheory.PreGaloisCategory.functorToAction F).obj X ≅
                  Action.FintypeCat.ofMulAction (CategoryTheory.Aut F)
                    { carrier := CategoryTheory.Aut F ⧸ MulAction.stabilizer (CategoryTheory.Aut F) x,
                      str := CategoryTheory.PreGaloisCategory.fintypeQuotientStabilizer✝ x }