awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h_1 : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
X : C
XinI : X ∈ (↑I : Set C)
refine_2 :
  Eq.{w + 1} (α := Aut (F.obj X)) ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X : Aut (F.obj X))
    (1 : Aut (F.obj X))
⊢ Membership.mem (α := (fun (a : C) ↦ Aut (F.obj a)) X) (u X)
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X : Aut (F.obj X))

Tactic:
suffices h : autEmbedding F σ X = 1 by
      rw [h]
      exact (ho X XinI).right
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h_1 : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
X : C
XinI : X ∈ (↑I : Set C)
have : ∀ (this : Fintype (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI))), σ.hom.app X = 𝟙 (F.obj X)
⊢ σ.hom.app X = 𝟙 (F.obj X)

Tactic:
have : Fintype (fι ⟨X, XinI⟩) := Fintype.ofFinite _
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h_1 : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
X : C
XinI : X ∈ (↑I : Set C)
this : Fintype (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI))
h₁ :
  ∀ (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))
              _ _ _ (σ.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))
              _ _ _ (𝟙 (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 :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
⊢ σ.hom.app X = 𝟙 (F.obj X)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h_1 : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
X : C
XinI : X ∈ (↑I : Set C)
⊢ σ.hom.app X = 𝟙 (F.obj X)

Tactic:
have h : σ.hom.app X = 𝟙 (F.obj X) := by
      have : Fintype (fι ⟨X, XinI⟩) := Fintype.ofFinite _
      ext x
      obtain ⟨⟨j⟩, a, ha : F.map _ a = x⟩ := Limits.FintypeCat.jointly_surjective
        (Discrete.functor (ff ⟨X, XinI⟩) ⋙ F) _ (Limits.isColimitOfPreserves F (h4 ⟨X, XinI⟩)) x
      rw [FintypeCat.id_apply, ← ha, NatTrans.naturality_apply]
      simp [h ⟨(ff _) j, ⟨Set.range (ff ⟨X, XinI⟩), ⟨⟨_, rfl⟩, ⟨j, rfl⟩⟩⟩⟩]
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h_1 : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h_2 : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
X : C
XinI : X ∈ (↑I : Set C)
h : σ.hom.app X = 𝟙 (F.obj X)
⊢ Eq.{w + 1} (α := Aut (F.obj X)) ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X : Aut (F.obj X))
    (1 : Aut (F.obj X))

Tactic:
Iso.ext h

Premises used: CategoryTheory.Aut, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h_1 : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h_2 : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
X : C
XinI : X ∈ (↑I : Set C)
h : σ.hom.app X = 𝟙 (F.obj X)
⊢ Eq.{w + 1} (α := Aut (F.obj X)) ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X : Aut (F.obj X))
    (1 : Aut (F.obj X))

Tactic:
exact Iso.ext h

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S : Set (Aut F)
rw :
  (∃ t ⊆ S, IsOpen t ∧ 1 ∈ t) ↔
    ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S
⊢ Membership.mem (γ := Filter (Aut F)) (𝓝 1) S ↔
    ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_iff
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S : Set (Aut F)
⊢ (∃ t ⊆ S, IsOpen t ∧ 1 ∈ t) ↔
    ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S : Set (Aut F)
refine_1 :
  (∃ t ⊆ S, IsOpen t ∧ 1 ∈ t) →
    ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S
refine_2 :
  (∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S) →
    ∃ t ⊆ S, IsOpen t ∧ 1 ∈ t
⊢ (∃ t ⊆ S, IsOpen t ∧ 1 ∈ t) ↔
    ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
refine_1 :
  ∀ (I : Set C) (w : Fintype (↑I : Type u₁)) (hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X)
    (hmem : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ U),
    ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S
⊢ ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S

Tactic:
obtain ⟨I, _, hc, hmem⟩ := exists_set_ker_evaluation_subset_of_isOpen F hUone hUopen

Premises used: CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hmem : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ U
P : C := piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
refine_1 :
  ∀ (A : C) (a : (F.obj A).obj) (hgal : IsGalois.{u₁, u₂} A)
    (hbij :
      Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
        fun (f : A ⟶ P) ↦
        (@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) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
          a),
    ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S
⊢ ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S

Tactic:
obtain ⟨A, a, hgal, hbij⟩ := exists_galois_representative F P

Premises used: CategoryTheory.PreGaloisCategory.exists_galois_representative
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hmem : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ U
P : C := piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
A : C
a : (F.obj A).obj
hgal : IsGalois.{u₁, u₂} A
hbij :
  Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
    fun (f : A ⟶ P) ↦
    (@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) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
      a
⊢ ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S

Tactic:
⟨⟨A, a, hgal⟩, trivial, ?_⟩

Premises used: trivial, And.intro, Exists.intro, CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hmem : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ U
P : C := piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
A : C
a : (F.obj A).obj
hgal : IsGalois.{u₁, u₂} A
hbij :
  Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
    fun (f : A ⟶ P) ↦
    (@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) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
      a
refine_1 :
  (↑(MulAction.stabilizer (Aut F) { obj := A, pt := a, isGalois := hgal : PointedGaloisObject F }.pt) : Set (Aut F)) ⊆ S
⊢ ∃ (i : PointedGaloisObject F), True ∧ (↑(MulAction.stabilizer (Aut F) i.pt) : Set (Aut F)) ⊆ S

Tactic:
refine ⟨⟨A, a, hgal⟩, trivial, ?_⟩
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hmem : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ U
P : C := piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
A : C
a : (F.obj A).obj
hgal : IsGalois.{u₁, u₂} A
hbij :
  Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
    fun (f : A ⟶ P) ↦
    (@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) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
      a
t : Aut F
refine_1 :
  ∀
    (ht :
      (@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 A) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
          a =
        a),
    t ∈ S
⊢ t ∈
      (↑(MulAction.stabilizer (Aut F) { obj := A, pt := a, isGalois := hgal : PointedGaloisObject F }.pt) :
        Set (Aut F)) →
    t ∈ S

Tactic:
(ht : t.hom.app A a = a)
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hmem : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ U
P : C := piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
A : C
a : (F.obj A).obj
hgal : IsGalois.{u₁, u₂} A
hbij :
  Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
    fun (f : A ⟶ P) ↦
    (@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) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
      a
t : Aut F
ht :
  (@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 A) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    a
refine_1 : t ∈ U
⊢ t ∈ S

Tactic:
apply hU
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hmem : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ U
P : C := piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
A : C
a : (F.obj A).obj
hgal : IsGalois.{u₁, u₂} A
hbij :
  Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
    fun (f : A ⟶ P) ↦
    (@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) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
      a
t : Aut F
ht :
  (@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 A) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    a
refine_1 : ∀ (X : (↑I : Type u₁)), t.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
⊢ t ∈ U

Tactic:
apply hmem
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hmem : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ U
P : C := piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
A : C
a : (F.obj A).obj
hgal : IsGalois.{u₁, u₂} A
hbij :
  Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
    fun (f : A ⟶ P) ↦
    (@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) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
      a
t : Aut F
ht :
  (@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 A) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    a
⊢ ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)

Tactic:
haveI (X : I) : IsConnected X.val := hc X.val X.property