-- Mathlib/CategoryTheory/Galois/IsFundamentalgroup.lean
lemma toAut_continuous [TopologicalSpace G] [IsTopologicalGroup G]
    [∀ (X : C), ContinuousSMul G (F.obj X)] :
    Continuous (toAut F G)

Proof state:
case hf
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
⊢ ∀ A ∈ nhds 1, ⇑(toAut F G) ⁻¹' A ∈ nhds 1

Tactic:
intro A hA

Result:
case hf
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
A : Set (Aut F)
hA : A ∈ nhds 1
⊢ ⇑(toAut F G) ⁻¹' A ∈ nhds 1

Proof state:
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
⊢ Continuous ⇑(toAut F G)

Tactic:
apply continuous_of_continuousAt_one

Result:
case hf
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
⊢ ContinuousAt (⇑(toAut F G)) 1

Proof state:
case hf
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
A : Set (Aut F)
hA : A ∈ nhds 1
⊢ ⇑(toAut F G) ⁻¹' A ∈ nhds 1

Tactic:
obtain ⟨X, _, hX⟩ := ((nhds_one_has_basis_stabilizers F).mem_iff' A).mp hA

Result:
case hf.intro.intro
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
A : Set (Aut F)
hA : A ∈ nhds 1
X : PointedGaloisObject F
left✝ : True
hX : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ A
⊢ ⇑(toAut F G) ⁻¹' A ∈ nhds 1

Proof state:
case hf.intro.intro
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
A : Set (Aut F)
hA : A ∈ nhds 1
X : PointedGaloisObject F
left✝ : True
hX : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ A
⊢ ⇑(toAut F G) ⁻¹' A ∈ nhds 1

Tactic:
rw [mem_nhds_iff]

Result:
case hf.intro.intro
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
A : Set (Aut F)
hA : A ∈ nhds 1
X : PointedGaloisObject F
left✝ : True
hX : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ A
⊢ ∃ t ⊆ ⇑(toAut F G) ⁻¹' A, IsOpen t ∧ 1 ∈ t

Proof state:
case hf
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
⊢ ContinuousAt (⇑(toAut F G)) 1

Tactic:
rw [continuousAt_def, map_one]

Result:
case hf
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
⊢ ∀ A ∈ nhds 1, ⇑(toAut F G) ⁻¹' A ∈ nhds 1

Proof state:
case hf.intro.intro
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
A : Set (Aut F)
hA : A ∈ nhds 1
X : PointedGaloisObject F
left✝ : True
hX : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ A
⊢ ∃ t ⊆ ⇑(toAut F G) ⁻¹' A, IsOpen t ∧ 1 ∈ t

Tactic:
exact ⟨MulAction.stabilizer G X.pt, Set.preimage_mono (f := toAut F G) hX,
  stabilizer_isOpen G X.pt, one_mem _⟩

Result:
no goals