{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          {X A : C} →
            {u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X} →
              {a : (F.obj A).carrier} →
                (CategoryTheory.ConcreteCategory.hom (F.map u)) a =
                    CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X →
                  [CategoryTheory.PreGaloisCategory.IsConnected A] →
                    (F.obj A).carrier → (F.obj X).carrier ≃ (F.obj X).carrier