awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
σ τ : Aut F
hst : σ ≈ τ
J' : SingleObj.{u₁}
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))) ⥤
  Action FintypeCat (Aut F) :=
  quotientDiag V h u ⋙ functorToAction F
m : End (C :=
  SingleObj.{u₁}
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
  (SingleObj.star
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))) :=
  ⟦Subtype.mk (p := fun (x : Aut F) ↦ x ∈ (↑V : Subgroup (Aut F))) (σ⁻¹ * τ) ⋯⟧
⊢ J'.map m ≫
      s.ι.app
        (SingleObj.star
          (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
            ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))) =
    s.ι.app
      (SingleObj.star
        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))

Tactic:
have h1 : J'.map m ≫ s.ι.app (SingleObj.star _) = s.ι.app (SingleObj.star _) :=
        s.ι.naturality m
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
g σ : Aut F
⊢ Eq (α :=
    ((functorToAction F).obj A).V ⟶
      (obj (C :=
          SingleObj.{u₁}
            (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
              ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
          (obj
            (const
              (SingleObj.{u₁}
                (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                  ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))))
            s.pt)
          (SingleObj.star
            (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
              ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))).V)
    ((((functorToAction F).obj A).ρ : (a : Aut F) → End ((functorToAction F).obj A).V) g ≫
        Action.Hom.hom
          (s.ι.app
            (SingleObj.star
              (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))) :
      ((functorToAction F).obj A).V ⟶
        (obj (C :=
            SingleObj.{u₁}
              (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
            (obj
              (const
                (SingleObj.{u₁}
                  (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                    ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))))
              s.pt)
            (SingleObj.star
              (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))).V)
    (Action.Hom.hom
          (s.ι.app
            (SingleObj.star
              (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))) ≫
        (s.pt.ρ : (a : Aut F) → End s.pt.V) g :
      ((quotientDiag V h u ⋙ functorToAction F).obj
            (SingleObj.star
              (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))).V ⟶
        s.pt.V)

Tactic:
have : ((functorToAction F).obj A).ρ g ≫ (s.ι.app (SingleObj.star _)).hom =
        (s.ι.app (SingleObj.star _)).hom ≫ s.pt.ρ g :=
      (s.ι.app (SingleObj.star _)).comm g
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
j :
  SingleObj.{u₁}
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))
apply :
  u.inv ≫ NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s =
    u.inv ≫ s.ι.app j
⊢ NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s = s.ι.app j

Tactic:
apply (cancel_epi u.inv).mp

Premises used: Iff.mp, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
j :
  SingleObj.{u₁}
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))
h₁ :
  Action.Hom.hom
      (u.inv ≫ NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s) =
    (u.inv ≫ s.ι.app j).hom
⊢ u.inv ≫ NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s =
    u.inv ≫ s.ι.app j

Tactic:
apply Action.hom_ext

Premises used: Action.hom_ext
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
j :
  SingleObj.{u₁}
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))
h₁ :
  ∀ (x : Aut F ⧸ (↑U : Subgroup (Aut F))),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
      ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _
              (Action.Hom.hom
                  (u.inv ≫
                    NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s) :
                Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
                  s.pt.V) :
            (a :
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                  (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
      ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (u.inv ≫ s.ι.app j).hom :
            (a :
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                  (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
⊢ Action.Hom.hom
      (u.inv ≫ NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ coconeQuotientDiagDesc h u hUinV s) =
    (u.inv ≫ s.ι.app j).hom

Tactic:
ext (x : Aut F ⧸ U.toSubgroup)

Premises used: CategoryTheory.Aut, OpenSubgroup.toSubgroup
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
f : Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV) ⟶ s.pt
hf :
  ∀
    (j :
      SingleObj.{u₁}
        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))),
    NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ f = s.ι.app j
h₁ : f.hom = (coconeQuotientDiagDesc h u hUinV s).hom
⊢ f = coconeQuotientDiagDesc h u hUinV s

Tactic:
apply Action.hom_ext

Premises used: Action.hom_ext
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
f : Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV) ⟶ s.pt
hf :
  ∀
    (j :
      SingleObj.{u₁}
        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))),
    NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ f = s.ι.app j
h₁ :
  ∀ (x : Aut F ⧸ (↑V : Subgroup (Aut F))),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
      ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ f.hom :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (coconeQuotientDiag h u hUinV).pt.V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
      ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (coconeQuotientDiagDesc h u hUinV s).hom :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (coconeQuotientDiag h u hUinV).pt.V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
⊢ f.hom = (coconeQuotientDiagDesc h u hUinV s).hom

Tactic:
ext (x : Aut F ⧸ V.toSubgroup)

Premises used: CategoryTheory.Aut, OpenSubgroup.toSubgroup
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
f : Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV) ⟶ s.pt
hf :
  ∀
    (j :
      SingleObj.{u₁}
        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))),
    NatTrans.app (Cocone.ι (coconeQuotientDiag h u hUinV)) j ≫ f = s.ι.app j
σ : Aut F
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ f.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (coconeQuotientDiag h u hUinV).pt.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
        ⟦σ⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (coconeQuotientDiagDesc h u hUinV s).hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (coconeQuotientDiag h u hUinV).pt.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
        ⟦σ⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)

Tactic:
simp [← hf (SingleObj.star _), ← ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.SingleObj.star
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
obtain :
  ∀ (I : Set C) (hf : Fintype (↑I : Type u₁)) (hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X)
    (hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))),
    ∃ (X : C),
      Nonempty.{u₁ + 1}
        ((functorToAction F).obj X ≅
          Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))

Tactic:
obtain ⟨I, hf, hc, hi⟩ := exists_set_ker_evaluation_subset_of_isOpen F (one_mem V) V.isOpen'

Premises used: CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen, OpenSubgroup.isOpen', OneMemClass.one_mem
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
⊢ ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)

Tactic:
haveI (X : I) : IsConnected X.val := hc X X.property
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
⊢ ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj

Tactic:
haveI (X : I) : Nonempty (F.obj X.val) := nonempty_fiber_of_isConnected F X
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
⊢ Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj

Tactic:
have hn : Nonempty (F.obj <| (∏ᶜ fun X : I => X)) := nonempty_fiber_pi_of_nonempty_of_finite F _
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
obtain :
  ∀ (A : C) (f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) (hgal : IsGalois.{u₁, u₂} A),
    ∃ (X : C),
      Nonempty.{u₁ + 1}
        ((functorToAction F).obj X ≅
          Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))

Tactic:
obtain ⟨A, f, hgal⟩ := exists_hom_from_galois_of_fiber_nonempty F (∏ᶜ fun X : I => X) hn

Premises used: CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber_nonempty, CategoryTheory.Limits.piObj, Subtype.val
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
obtain :
  ∀ (a : (F.obj A).obj),
    ∃ (X : C),
      Nonempty.{u₁ + 1}
        ((functorToAction F).obj X ≅
          Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Premises used: CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
⊢ (↑U : Subgroup (Aut F)).Normal

Tactic:
have hUnormal : U.toSubgroup.Normal := stabilizer_normal_of_isGalois F A a