awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
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
⊢ (Set.univ ∩ c).Nonempty
have htc : ∀ (i : PointedGaloisObject F), IsClosed (cl i)
Tactic: apply CompactSpace.isCompact_univ.inter_iInter_nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
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
htc : ∀ (i : PointedGaloisObject F), IsClosed (cl i)
⊢ (Set.univ ∩ c).Nonempty
have hst : ∀ (u : Finset (PointedGaloisObject F)), Set.Nonempty.{u_1} (α := G) (Set.univ ∩ ⋂ i ∈ u, cl i)
Tactic: apply CompactSpace.isCompact_univ.inter_iInter_nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
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 : PointedGaloisObject F
⊢ IsClosed (cl X)
have htc : IsClosed (↑(MulAction.stabilizer G X.pt) : Set G)
Tactic: apply IsClosed.leftCoset
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
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)
⊢ Set.Nonempty.{u_1} (α := G) (Set.univ ∩ ⋂ i ∈ s, cl i)
have hst : Set.Nonempty.{u_1} (α := G) (⋂ i ∈ s, cl i)
Tactic: rw [Set.univ_inter]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
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)
⊢ Set.Nonempty.{u_1} (α := G) (⋂ i ∈ s, cl i)
have 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)
Tactic: obtain ⟨gs, hgs⟩ :=
        toAut_surjective_isGalois_finite_family F G t (fun X : s ↦ X.val.obj) h
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
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
⊢ Set.Nonempty.{u_1} (α := G) (⋂ i ∈ s, cl i)
have h₁ : Membership.mem (γ := Set G) (⋂ i ∈ s, cl i) gs
Tactic: use gs
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
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
⊢ Membership.mem (γ := Set G) (⋂ i ∈ s, cl i) gs
have h₁ : ∀ (i : PointedGaloisObject F) (i_1 : i ∈ s), gs ∈ cl i
Tactic: simp only [Set.mem_iInter]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
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
X : PointedGaloisObject F
hXmem : X ∈ s
⊢ gs ∈ cl X
have h₁ : (gi X)⁻¹ * gs ∈ (↑(MulAction.stabilizer G X.pt) : Set G)
Tactic: rw [mem_leftCoset_iff, SetLike.mem_coe, MulAction.mem_stabilizer_iff, mul_smul,
        hgs ⟨X, hXmem⟩, ← hgi X, inv_smul_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
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
X : PointedGaloisObject F
hXmem : X ∈ s
h₁ : (gi X)⁻¹ * gs ∈ (↑(MulAction.stabilizer G X.pt) : Set G)
⊢ gs ∈ cl X
have h₂ : Membership.mem (γ := Subgroup G) (MulAction.stabilizer G X.pt) ((gi X)⁻¹ * gs)
Tactic: rw [mem_leftCoset_iff, SetLike.mem_coe, MulAction.mem_stabilizer_iff, mul_smul,
        hgs ⟨X, hXmem⟩, ← hgi X, inv_smul_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
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
X : PointedGaloisObject F
hXmem : X ∈ s
h₁ : (gi X)⁻¹ * gs ∈ (↑(MulAction.stabilizer G X.pt) : Set G)
h₂ : Membership.mem (γ := Subgroup G) (MulAction.stabilizer G X.pt) ((gi X)⁻¹ * gs)
⊢ gs ∈ cl X
have h₃ : ((gi X)⁻¹ * gs) • X.pt = X.pt
Tactic: rw [mem_leftCoset_iff, SetLike.mem_coe, MulAction.mem_stabilizer_iff, mul_smul,
        hgs ⟨X, hXmem⟩, ← hgi X, inv_smul_smul]