awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
s : Finset (PointedGaloisObject F)
hst : Set.Nonempty.{u_1} (α := G) (⋂ i ∈ s, cl i)
⊢ Set.Nonempty.{u_1} (α := G) (Set.univ ∩ ⋂ i ∈ s, cl i)

Tactic:
rw [Set.univ_inter]

Premises used: Set.univ_inter
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
s : Finset (PointedGaloisObject F)
hst :
  ∀ (gs : G)
    (hgs :
      ∀ (i : ↥s) (x : (F.obj (↑i : PointedGaloisObject F).obj).obj),
        gs • x =
          (@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))
                _ _ _
                (t.hom.app (↑i : PointedGaloisObject F).obj :
                  F.obj (↑i : PointedGaloisObject F).obj ⟶ F.obj (↑i : PointedGaloisObject F).obj) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑i : PointedGaloisObject F).obj)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑i : PointedGaloisObject F).obj))
            x),
    Set.Nonempty.{u_1} (α := G) (⋂ i ∈ s, cl i)
⊢ Set.Nonempty.{u_1} (α := G) (⋂ i ∈ s, cl i)

Tactic:
obtain ⟨gs, hgs⟩ :=
        toAut_surjective_isGalois_finite_family F G t (fun X : s ↦ X.val.obj) h

Premises used: CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family, CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj, Subtype.val
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs :
  ∀ (i : ↥s) (x : (F.obj (↑i : PointedGaloisObject F).obj).obj),
    gs • x =
      (@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))
            _ _ _
            (t.hom.app (↑i : PointedGaloisObject F).obj :
              F.obj (↑i : PointedGaloisObject F).obj ⟶ F.obj (↑i : PointedGaloisObject F).obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑i : PointedGaloisObject F).obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑i : PointedGaloisObject F).obj))
        x
h₁ : Membership.mem (γ := Set G) (⋂ i ∈ s, cl i) gs
⊢ Set.Nonempty.{u_1} (α := G) (⋂ i ∈ s, cl i)

Tactic:
use gs
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs :
  ∀ (i : ↥s) (x : (F.obj (↑i : PointedGaloisObject F).obj).obj),
    gs • x =
      (@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))
            _ _ _
            (t.hom.app (↑i : PointedGaloisObject F).obj :
              F.obj (↑i : PointedGaloisObject F).obj ⟶ F.obj (↑i : PointedGaloisObject F).obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑i : PointedGaloisObject F).obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑i : PointedGaloisObject F).obj))
        x
h₁ : ∀ (i : PointedGaloisObject F) (i_1 : i ∈ s), gs ∈ cl i
⊢ Membership.mem (γ := Set G) (⋂ i ∈ s, cl i) gs

Tactic:
simp only [Set.mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
⊢ c.Nonempty

Tactic:
have hne : c.Nonempty := by
    rw [← Set.univ_inter c]
    apply CompactSpace.isCompact_univ.inter_iInter_nonempty
    · intro X
      apply IsClosed.leftCoset
      exact Subgroup.isClosed_of_isOpen _ (stabilizer_isOpen G X.pt)
    · intro s
      rw [Set.univ_inter]
      obtain ⟨gs, hgs⟩ :=
        toAut_surjective_isGalois_finite_family F G t (fun X : s ↦ X.val.obj) h
      use gs
      simp only [Set.mem_iInter]
      intro X hXmem
      rw [mem_leftCoset_iff, SetLike.mem_coe, MulAction.mem_stabilizer_iff, mul_smul,
        hgs ⟨X, hXmem⟩, ← hgi X, inv_smul_smul]
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
hne : c.Nonempty
obtain : ∀ (g : G) (hg : g ∈ c), ∃ (a : G), (toAut F G : (a : G) → Aut F) a = t
⊢ ∃ (a : G), (toAut F G : (a : G) → Aut F) a = t

Tactic:
obtain ⟨g, hg⟩ := hne
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
g : G
hg : g ∈ c
⊢ ∃ (a : G), (toAut F G : (a : G) → Aut F) a = t

Tactic:
⟨g, Iso.ext <| natTrans_ext_of_isGalois _ <| fun X _ ↦ ?_⟩

Premises used: Exists.intro, CategoryTheory.Iso.ext, CategoryTheory.PreGaloisCategory.natTrans_ext_of_isGalois
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
g : G
hg : g ∈ c
refine : ∀ (X : C), IsGalois.{u₁, u₂} X → NatTrans.app (Iso.hom ((toAut F G : (a : G) → Aut F) g)) X = t.hom.app X
⊢ ∃ (a : G), (toAut F G : (a : G) → Aut F) a = t

Tactic:
refine ⟨g, Iso.ext <| natTrans_ext_of_isGalois _ <| fun X _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
g : G
hg : g ∈ c
X : C
h_1 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
⊢ ∀ (i : PointedGaloisObject F), g ∈ cl i

Tactic:
simp only [Set.mem_iInter, c] at hg

Premises used: Set.mem_iInter
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
g : G
X : C
h_1 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
hg : ∀ (i : PointedGaloisObject F), g ∈ cl i
⊢ g ∈ gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • (↑(MulAction.stabilizer G x) : Set G)

Tactic:
hg _

Premises used: Set.Mem, setOf
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
g : G
X : C
h_1 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
hg : ∀ (i : PointedGaloisObject F), g ∈ cl i
⊢ g ∈ gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • (↑(MulAction.stabilizer G x) : Set G)

Tactic:
exact hg _
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
g : G
hg : g ∈ c
X : C
h_1 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
⊢ g ∈ gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • (↑(MulAction.stabilizer G x) : Set G)

Tactic:
have : g ∈ (gi ⟨X, x, inferInstance⟩ • MulAction.stabilizer G x : Set G) := by
    simp only [Set.mem_iInter, c] at hg
    exact hg _