∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {A B : C}
  [inst_2 : CategoryTheory.PreGaloisCategory.IsGalois A] [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois B]
  (f : A ⟶ B), Function.Surjective (CategoryTheory.PreGaloisCategory.autMap f)