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
g : G
hg : g ∈ c
X : C
h_1 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
this : g ∈ gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • (↑(MulAction.stabilizer G x) : Set G)
h₁ :
  ∀ (s : G) (hsmem : s • x = x) (hg : gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • s ∈ c),
    (gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • s) • 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) :
          (a : (F.obj X).obj) → (F.obj X).obj)
        x
⊢ g • 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) :
        (a : (F.obj X).obj) → (F.obj X).obj)
      x

Tactic:
obtain ⟨s, (hsmem : s • x = x), (rfl : gi ⟨X, x, inferInstance⟩ • s = _)⟩ := this

Premises used: inferInstance, CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk, rfl
-- 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
X : C
h_1 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
s : G
hsmem : s • x = x
hg : gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • s ∈ c
h₁ :
  gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • 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) :
        (a : (F.obj X).obj) → (F.obj X).obj)
      x
⊢ (gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • s) • 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) :
        (a : (F.obj X).obj) → (F.obj X).obj)
      x

Tactic:
rw [smul_eq_mul, mul_smul, hsmem]

Premises used: smul_eq_mul, SemigroupAction.mul_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
X : C
h_1 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
s : G
hsmem : s • x = x
hg : gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • s ∈ c
⊢ gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • 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) :
        (a : (F.obj X).obj) → (F.obj X).obj)
      x

Tactic:
hgi ⟨X, x, inferInstance⟩ x

Premises used: inferInstance, CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk
-- 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
X : C
h_1 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
s : G
hsmem : s • x = x
hg : gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • s ∈ c
⊢ gi { obj := X, pt := x, isGalois := ⋯ : PointedGaloisObject F } • 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) :
        (a : (F.obj X).obj) → (F.obj X).obj)
      x

Tactic:
exact hgi ⟨X, x, inferInstance⟩ x

Premises used: inferInstance, CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk
-- 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
h : Function.Surjective (α := G) (β := Aut F) (⇑(toAut F G) : (a : G) → Aut F)
X : C
inst_6 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
obtain : ∀ (t : Aut F) (ht : t • x = y), ∃ (g : G), g • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
obtain ⟨t, ht⟩ := MulAction.exists_smul_eq (Aut F) x y

Premises used: CategoryTheory.Aut, MulAction.exists_smul_eq
-- 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
h : Function.Surjective (α := G) (β := Aut F) (⇑(toAut F G) : (a : G) → Aut F)
X : C
inst_6 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
t : Aut F
ht : t • x = y
obtain : ∀ (g : G) (ht : HSMul.hSMul (α := Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F) x = y), ∃ (g : G), g • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
obtain ⟨g, rfl⟩ := h t

Premises used: rfl
-- 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
h : Function.Surjective (α := G) (β := Aut F) (⇑(toAut F G) : (a : G) → Aut F)
X : C
inst_6 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
g : G
ht : HSMul.hSMul (α := Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F) x = y
⊢ ∃ (g : G), g • x = y

Tactic:
⟨g, ht⟩

Premises used: Exists.intro
-- 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
h : Function.Surjective (α := G) (β := Aut F) (⇑(toAut F G) : (a : G) → Aut F)
X : C
inst_6 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
g : G
ht : HSMul.hSMul (α := Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F) x = y
⊢ ∃ (g : G), g • x = y

Tactic:
exact ⟨g, ht⟩
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
inst_7 : IsFundamentalGroup F G
g : G
h : ∀ (X : C) (x : (F.obj X).obj), g • x = x
⊢ g = 1

Tactic:
IsFundamentalGroup.non_trivial' g h

Premises used: CategoryTheory.PreGaloisCategory.IsFundamentalGroup.non_trivial'
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
g : Aut F
h : ∀ (X : C) (x : (F.obj X).obj), g • x = x
h₁ :
  ∀ (X : C) (x : (F.obj X).obj),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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))
              _ _ _ (g.hom.app X) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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))
              _ _ _ (NatTrans.app (Iso.hom 1) X : F.obj X ⟶ F.obj X) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
⊢ g = 1

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
g : Aut F
h : ∀ (X : C) (x : (F.obj X).obj), g • x = x
X : C
x : (F.obj X).obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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))
            _ _ _ (g.hom.app X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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))
            _ _ _ (NatTrans.app (Iso.hom 1) X : F.obj X ⟶ F.obj X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))

Tactic:
h X x
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
g : Aut F
h : ∀ (X : C) (x : (F.obj X).obj), g • x = x
X : C
x : (F.obj X).obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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))
            _ _ _ (g.hom.app X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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))
            _ _ _ (NatTrans.app (Iso.hom 1) X : F.obj X ⟶ F.obj X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))

Tactic:
exact h X x
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
inst_5 : TopologicalSpace G
inst_6 : IsTopologicalGroup G
inst_7 : CompactSpace G
inst_8 : IsFundamentalGroup F G
X : C
inst_9 : IsConnected.{u₁, u₂} X
⊢ MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj

Tactic:
isPretransitive_of_surjective F G (toAut_bijective F G).surjective X

Premises used: CategoryTheory.PreGaloisCategory.isPretransitive_of_surjective, Function.Bijective.surjective, CategoryTheory.PreGaloisCategory.toAut_bijective
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
inst_5 : TopologicalSpace G
inst_6 : IsTopologicalGroup G
inst_7 : CompactSpace G
inst_8 : IsFundamentalGroup F G
rw :
  Continuous (X := G) (Y := Aut F) (⇑(toAut F G) : (a : G) → Aut F) ∧
    Function.Bijective (α := G) (β := Aut F) (⇑(toAut F G) : (a : G) → Aut F)
⊢ IsHomeomorph (X := G) (Y := Aut F) (⇑(toAut F G) : (a : G) → Aut F)

Tactic:
rw [isHomeomorph_iff_continuous_bijective]

Premises used: isHomeomorph_iff_continuous_bijective
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
inst_5 : TopologicalSpace G
inst_6 : IsTopologicalGroup G
inst_7 : CompactSpace G
inst_8 : IsFundamentalGroup F G
⊢ Continuous (X := G) (Y := Aut F) (⇑(toAut F G) : (a : G) → Aut F) ∧
    Function.Bijective (α := G) (β := Aut F) (⇑(toAut F G) : (a : G) → Aut F)

Tactic:
⟨toAut_continuous F G, toAut_bijective F G⟩

Premises used: And.intro, CategoryTheory.PreGaloisCategory.toAut_bijective, CategoryTheory.PreGaloisCategory.toAut_continuous
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
inst_5 : TopologicalSpace G
inst_6 : IsTopologicalGroup G
inst_7 : CompactSpace G
inst_8 : IsFundamentalGroup F G
⊢ Continuous (X := G) (Y := Aut F) (⇑(toAut F G) : (a : G) → Aut F) ∧
    Function.Bijective (α := G) (β := Aut F) (⇑(toAut F G) : (a : G) → Aut F)

Tactic:
exact ⟨toAut_continuous F G, toAut_bijective F G⟩
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
inst_5 : TopologicalSpace G
inst_6 : IsTopologicalGroup G
inst_7 : CompactSpace G
inst_8 : IsFundamentalGroup F G
⊢ IsHomeomorph (X := G) (Y := Aut F) (⇑(toAutMulEquiv F G) : (a : G) → Aut F)

Tactic:
toAut_isHomeomorph F G

Premises used: CategoryTheory.PreGaloisCategory.toAut_isHomeomorph, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
inst_5 : TopologicalSpace G
inst_6 : IsTopologicalGroup G
inst_7 : CompactSpace G
inst_8 : IsFundamentalGroup F G
g : G
⊢ Eq (α := Aut F) ((toAutMulEquiv F G : (a : G) → Aut F) g : Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F)

Tactic:
rfl

Premises used: rfl, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
inst_5 : TopologicalSpace G
inst_6 : IsTopologicalGroup G
inst_7 : CompactSpace G
inst_8 : IsFundamentalGroup F G
g : G
⊢ Eq (α := Aut F) ((toAutHomeo F G : (a : G) → Aut F) g : Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F)

Tactic:
rfl

Premises used: rfl, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
A B : PointedGaloisObject F
f g : A ⟶ B
h : f.val = g.val
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.ext