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
g : G
X Y : C
f : X ⟶ Y
h :
  ∀ (x : (F.obj X).obj),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
      ((@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.map f ≫ (isoOnObj F g Y).hom) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
      ((@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))
              _ _ _ ((isoOnObj F g X).hom ≫ F.map f) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
⊢ F.map f ≫ (isoOnObj F g Y).hom = (isoOnObj F g X).hom ≫ F.map f

Tactic:
ext
-- 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
g : G
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    ((@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.map f ≫ (isoOnObj F g Y).hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    ((@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))
            _ _ _ ((isoOnObj F g X).hom ≫ F.map f) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))

Tactic:
(IsNaturalSMul.naturality _ _ _).symm

Premises used: CategoryTheory.PreGaloisCategory.IsNaturalSMul.naturality, Eq.symm
-- 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
g : G
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    ((@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.map f ≫ (isoOnObj F g Y).hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    ((@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))
            _ _ _ ((isoOnObj F g X).hom ≫ F.map f) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))

Tactic:
exact (IsNaturalSMul.naturality _ _ _).symm

Premises used: CategoryTheory.PreGaloisCategory.IsNaturalSMul.naturality, Eq.symm
-- 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
h :
  ∀ (x : C) (x_1 : (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))
              _ _ _ ((NatIso.ofComponents (isoOnObj.{u₁, u₂, w, u_1} F (G := G) 1) ⋯).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_1 :
        (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_1 :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj x))
⊢ NatIso.ofComponents (isoOnObj.{u₁, u₂, w, u_1} F (G := G) 1) ⋯ = 1

Tactic:
ext
-- 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
x : C
x_1 : (F.obj x).obj
h :
  HSMul.hSMul.{u_1, w, w} (α := G) 1 x_1 =
    (@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 : (F.obj x).obj) → (F.obj x).obj)
      x_1
⊢ 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))
            _ _ _ ((NatIso.ofComponents (isoOnObj.{u₁, u₂, w, u_1} F (G := G) 1) ⋯).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_1 :
      (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_1 :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj x))

Tactic:
dsimp [isoOnObj]

Premises used: _private.0.CategoryTheory.PreGaloisCategory.isoOnObj
-- 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
g h : G
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))
              _ _ _ ((NatIso.ofComponents (isoOnObj F (g * h)) ⋯).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))
              _ _ _ ((NatIso.ofComponents (isoOnObj F g) ⋯ * NatIso.ofComponents (isoOnObj F h) ⋯).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))
⊢ NatIso.ofComponents (isoOnObj F (g * h)) ⋯ =
    NatIso.ofComponents (isoOnObj F g) ⋯ * NatIso.ofComponents (isoOnObj F h) ⋯

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
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
g h : G
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))
            _ _ _ ((NatIso.ofComponents (isoOnObj F (g * h)) ⋯).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))
            _ _ _ ((NatIso.ofComponents (isoOnObj F g) ⋯ * NatIso.ofComponents (isoOnObj F h) ⋯).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))

Tactic:
apply mul_smul

Premises used: 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
g : G
X : C
x : (F.obj X).obj
⊢ (@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 ((toAut F G : (a : G) → Aut F) g)) 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 =
    g • x

Tactic:
rfl

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
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
rw : LE.le (α := Subgroup G) (MonoidHom.ker (toAut F G)) ⊥
⊢ Function.Injective (α := G) (β := Aut F) (⇑(toAut F G) : (a : G) → Aut F)

Tactic:
rw [← MonoidHom.ker_eq_bot_iff, eq_bot_iff]

Premises used: MonoidHom.ker_eq_bot_iff, eq_bot_iff
-- 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
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
g : G
toAut :
  ∀ (hg : Eq (α := Aut F) ((PreGaloisCategory.toAut F G : (a : G) → Aut F) g : Aut F) (1 : Aut F)),
    Membership.mem (γ := Subgroup G) ⊥ g
⊢ Membership.mem (γ := Subgroup G) (MonoidHom.ker (PreGaloisCategory.toAut F G)) g →
    Membership.mem (γ := Subgroup G) ⊥ g

Tactic:
(hg : toAut F G g = 1)
-- 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
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
g : G
hg : Eq (α := Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F) (1 : Aut F)
⊢ Membership.mem (γ := Subgroup G) ⊥ g

Tactic:
h g (fun X x ↦ ?_)

Premises used: Set.Mem, setOf, Set.singleton
-- 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
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
g : G
hg : Eq (α := Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F) (1 : Aut F)
refine : ∀ (X : C) (x : (F.obj X).obj), g • x = x
⊢ Membership.mem (γ := Subgroup G) ⊥ g

Tactic:
refine h g (fun 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
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
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
g : G
hg : Eq (α := Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F) (1 : Aut F)
X : C
x : (F.obj X).obj
rw : NatTrans.app (Iso.hom 1) X = 𝟙 (F.obj X)
⊢ NatTrans.app (Iso.hom ((toAut F G : (a : G) → Aut F) g)) X = 𝟙 (F.obj X)

Tactic:
rw [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
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
g : G
hg : Eq (α := Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F) (1 : Aut F)
X : C
x : (F.obj X).obj
⊢ NatTrans.app (Iso.hom 1) X = 𝟙 (F.obj X)

Tactic:
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
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
g : G
hg : Eq (α := Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F) (1 : Aut F)
X : C
x : (F.obj X).obj
⊢ NatTrans.app (Iso.hom ((toAut F G : (a : G) → Aut F) g)) X = 𝟙 (F.obj X)

Tactic:
have : (toAut F G g).hom.app X = 𝟙 (F.obj X) := by
    rw [hg]
    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
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
g : G
hg : Eq (α := Aut F) ((toAut F G : (a : G) → Aut F) g : Aut F) (1 : Aut F)
X : C
x : (F.obj X).obj
this : NatTrans.app (Iso.hom ((toAut F G : (a : G) → Aut F) g)) X = 𝟙 (F.obj X)
rw :
  (@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 ((toAut F G : (a : G) → Aut F) g)) 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 =
    x
rw₁ :
  (@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.obj 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 =
    x
rw₂ rw₃ : x = x
⊢ g • x = x

Tactic:
rw [← toAut_hom_app_apply, this, FintypeCat.id_apply]

Premises used: CategoryTheory.PreGaloisCategory.toAut_hom_app_apply, FintypeCat.id_apply
-- 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 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
hf : ContinuousAt (X := G) (Y := Aut F) (⇑(toAut F G) : (a : G) → Aut F) 1
⊢ Continuous (X := G) (Y := Aut F) (⇑(toAut F G) : (a : G) → Aut F)

Tactic:
apply continuous_of_continuousAt_one

Premises used: continuous_of_continuousAt_one
-- 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 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
hf :
  ∀ (A : Set (Aut F)),
    Membership.mem (γ := Filter (Aut F)) (nhds 1) A →
      Membership.mem (γ := Filter G) (nhds 1) ((⇑(toAut F G) : (a : G) → Aut F) ⁻¹' A)
⊢ ContinuousAt (X := G) (Y := Aut F) (⇑(toAut F G) : (a : G) → Aut F) 1

Tactic:
rw [continuousAt_def, map_one]

Premises used: map_one, continuousAt_def
-- 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 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
A : Set (Aut F)
hA : Membership.mem (γ := Filter (Aut F)) (nhds 1) A
hf :
  ∀ (X : PointedGaloisObject F),
    True →
      ∀ (hX : (↑(MulAction.stabilizer (Aut F) X.pt) : Set (Aut F)) ⊆ A),
        Membership.mem (γ := Filter G) (nhds 1) ((⇑(toAut F G) : (a : G) → Aut F) ⁻¹' A)
⊢ Membership.mem (γ := Filter G) (nhds 1) ((⇑(toAut F G) : (a : G) → Aut F) ⁻¹' A)

Tactic:
obtain ⟨X, _, hX⟩ := ((nhds_one_has_basis_stabilizers F).mem_iff' A).mp hA

Premises used: CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers, Iff.mp, Filter.HasBasis.mem_iff'
-- 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 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
A : Set (Aut F)
hA : Membership.mem (γ := Filter (Aut F)) (nhds 1) A
X : PointedGaloisObject F
left : True
hX : (↑(MulAction.stabilizer (Aut F) X.pt) : Set (Aut F)) ⊆ A
hf : ∃ t ⊆ (⇑(toAut F G) : (a : G) → Aut F) ⁻¹' A, IsOpen t ∧ 1 ∈ t
⊢ Membership.mem (γ := Filter G) (nhds 1) ((⇑(toAut F G) : (a : G) → Aut F) ⁻¹' A)

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_iff