∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A B : C}
  [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsConnected B]
  (a : (F.obj A).carrier) (b : (F.obj B).carrier) (i : A ⟶ X) (j : B ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (F.map i)) a = (CategoryTheory.ConcreteCategory.hom (F.map j)) b →
    ∀ [CategoryTheory.Mono i] [CategoryTheory.Mono j], ∃ f, (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) a = b