-- Mathlib/CategoryTheory/Galois/Topology.lean
/-- The stabilizers of points in the fibers of Galois objects form a neighbourhood basis
of the identity in `Aut F`. -/
lemma nhds_one_has_basis_stabilizers : (nhds (1 : Aut F)).HasBasis (fun _ ↦ True)
    (fun X : PointedGaloisObject F ↦ MulAction.stabilizer (Aut F) X.pt) where
  mem_iff' S

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro.a.a
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X => ↑X
A : C
a : (F.obj A).carrier
hgal : IsGalois A
hbij : Function.Bijective fun f => F.map f a
t : Aut F
ht : t.hom.app A a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
X : ↑I
⊢ t.hom.app ↑X = 𝟙 (F.obj ↑X)

Tactic:
ext x

Result:
case refine_1.intro.intro.intro.intro.intro.intro.a.a.h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X => ↑X
A : C
a : (F.obj A).carrier
hgal : IsGalois A
hbij : Function.Bijective fun f => F.map f a
t : Aut F
ht : t.hom.app A a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
X : ↑I
x : (F.obj ↑X).carrier
⊢ t.hom.app (↑X) x = 𝟙 (F.obj ↑X) x

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro.a
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X => ↑X
A : C
a : (F.obj A).carrier
hgal : IsGalois A
hbij : Function.Bijective fun f => F.map f a
t : Aut F
ht : t.hom.app A a = a
⊢ t ∈ U

Tactic:
apply hmem

Result:
case refine_1.intro.intro.intro.intro.intro.intro.a.a
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X => ↑X
A : C
a : (F.obj A).carrier
hgal : IsGalois A
hbij : Function.Bijective fun f => F.map f a
t : Aut F
ht : t.hom.app A a = a
⊢ ∀ (X : ↑I), t.hom.app ↑X = 𝟙 (F.obj ↑X)

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro.a.a
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X => ↑X
A : C
a : (F.obj A).carrier
hgal : IsGalois A
hbij : Function.Bijective fun f => F.map f a
t : Aut F
ht : t.hom.app A a = a
this : ∀ (X : ↑I), IsConnected ↑X
⊢ ∀ (X : ↑I), t.hom.app ↑X = 𝟙 (F.obj ↑X)

Tactic:
haveI (X : I) : Nonempty (F.obj X.val) := nonempty_fiber_of_isConnected F X

Result:
case refine_1.intro.intro.intro.intro.intro.intro.a.a
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X => ↑X
A : C
a : (F.obj A).carrier
hgal : IsGalois A
hbij : Function.Bijective fun f => F.map f a
t : Aut F
ht : t.hom.app A a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
⊢ ∀ (X : ↑I), t.hom.app ↑X = 𝟙 (F.obj ↑X)

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro.a.a.h.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X => ↑X
A : C
a : (F.obj A).carrier
hgal : IsGalois A
hbij : Function.Bijective fun f => F.map f a
t : Aut F
ht : t.hom.app A a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
X : ↑I
f : A ⟶ P
⊢ t.hom.app (↑X) (F.map (Pi.π (fun X => ↑X) X) ((fun f => F.map f a) f)) =
    F.map (Pi.π (fun X => ↑X) X) ((fun f => F.map f a) f)

Tactic:
rw [FunctorToFintypeCat.naturality, FunctorToFintypeCat.naturality, ht]

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
⊢ (∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S) → ∃ t ⊆ S, IsOpen t ∧ 1 ∈ t

Tactic:
intro ⟨X, _, h⟩

Result:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
X : PointedGaloisObject F
left✝ : True
h : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ S
⊢ ∃ t ⊆ S, IsOpen t ∧ 1 ∈ t

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
⊢ (∃ t ⊆ S, IsOpen t ∧ 1 ∈ t) ↔ ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
⊢ (∃ t ⊆ S, IsOpen t ∧ 1 ∈ t) → ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S

case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
⊢ (∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S) → ∃ t ⊆ S, IsOpen t ∧ 1 ∈ t