-- 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.h.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
z : (F.obj (∏ᶜ fun X => ↑X)).carrier
⊢ t.hom.app (↑X) (F.map (Pi.π (fun X => ↑X) X) z) = F.map (Pi.π (fun X => ↑X) X) z

Tactic:
obtain ⟨f, rfl⟩ := hbij.surjective z

Result:
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)

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)
X : PointedGaloisObject F
left✝ : True
h : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ S
⊢ ∃ t ⊆ S, IsOpen t ∧ 1 ∈ t

Tactic:
exact ⟨MulAction.stabilizer (Aut F) X.pt, h, stabilizer_isOpen (Aut F) X.pt,
  Subgroup.one_mem _⟩

Result:
no goals

Proof state:
case refine_1.intro.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
⊢ ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S

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

Result:
case refine_1.intro.intro.intro.intro.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
⊢ ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S

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

Tactic:
rw [mem_nhds_iff]

Result:
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

Proof state:
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

Tactic:
simp only [FintypeCat.id_apply]

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 = x

Proof state:
case refine_1.intro.intro.intro.intro.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
⊢ ↑(MulAction.stabilizer (Aut F) { obj := A, pt := a, isGalois := hgal }.pt) ⊆ S

Tactic:
intro t (ht : t.hom.app A a = a)

Result:
case refine_1.intro.intro.intro.intro.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
⊢ t ∈ S

Proof state:
case refine_1.intro.intro.intro.intro.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
⊢ t ∈ S

Tactic:
apply hU

Result:
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