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

Tactic:
obtain ⟨z, rfl⟩ :=
  surjective_of_nonempty_fiber_of_isConnected F (Pi.π (fun X : I ↦ X.val) X) x

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

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

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

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
⊢ ↑(MulAction.stabilizer (Aut F) { obj := A, pt := a, isGalois := hgal }.pt) ⊆ 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
⊢ ∀ (X : ↑I), t.hom.app ↑X = 𝟙 (F.obj ↑X)

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

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
⊢ ∀ (X : ↑I), t.hom.app ↑X = 𝟙 (F.obj ↑X)

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

Tactic:
let P : C := ∏ᶜ fun X : I ↦ X.val

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

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

Tactic:
intro ⟨U, hU, hUopen, hUone⟩

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

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

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