∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F),
  ↑((CategoryTheory.PreGaloisCategory.autGaloisSystem F).obj A) = CategoryTheory.Aut A.obj