-- Mathlib/CategoryTheory/Galois/IsFundamentalgroup.lean
/-- If `G` is a compact, topological group that acts continuously and naturally on the
fibers of `F`, `toAut F G` is surjective if and only if it acts transitively on the fibers
of all Galois objects. This is the `if` direction. For the `only if` see
`isPretransitive_of_surjective`. -/
lemma toAut_surjective_of_isPretransitive [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [∀ (X : C), ContinuousSMul G (F.obj X)]
    (h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X)) :
    Function.Surjective (toAut F G)

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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).carrier), gi X • x = t.hom.app X.obj x
⊢ ∃ a, (toAut F G) a = t

Tactic:
let cl (X : PointedGaloisObject F) : Set G := gi X • MulAction.stabilizer G X.pt

Result:
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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).carrier), gi X • x = t.hom.app X.obj x
cl : PointedGaloisObject F → Set G := fun X => gi X • ↑(MulAction.stabilizer G X.pt)
⊢ ∃ a, (toAut F G) a = t

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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).carrier), gi X • x = t.hom.app X.obj x
cl : PointedGaloisObject F → Set G := fun X => gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
hne : c.Nonempty
⊢ ∃ a, (toAut F G) a = t

Tactic:
obtain ⟨g, hg⟩ := hne

Result:
case 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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).carrier), gi X • x = t.hom.app X.obj x
cl : PointedGaloisObject F → Set G := fun X => gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
g : G
hg : g ∈ c
⊢ ∃ a, (toAut F G) a = t

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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).carrier), gi X • x = t.hom.app X.obj x
cl : PointedGaloisObject F → Set G := fun X => gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
⊢ (Set.univ ∩ c).Nonempty

Tactic:
apply CompactSpace.isCompact_univ.inter_iInter_nonempty

Result:
case htc
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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).carrier), gi X • x = t.hom.app X.obj x
cl : PointedGaloisObject F → Set G := fun X => gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
⊢ ∀ (i : PointedGaloisObject F), IsClosed (cl i)

case hst
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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).carrier), gi X • x = t.hom.app X.obj x
cl : PointedGaloisObject F → Set G := fun X => gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
⊢ ∀ (u : Finset (PointedGaloisObject F)), (Set.univ ∩ ⋂ i ∈ u, cl i).Nonempty

Proof state:
case intro.h.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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).carrier), gi X • x = t.hom.app X.obj x
cl : PointedGaloisObject F → Set G := fun X => gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
X : C
x✝ : IsGalois X
x : (F.obj X).carrier
s : G
hsmem : s • x = x
hg : gi { obj := X, pt := x, isGalois := ⋯ } • s ∈ c
⊢ (gi { obj := X, pt := x, isGalois := ⋯ } • s) • x = t.hom.app X x

Tactic:
rw [smul_eq_mul, mul_smul, hsmem]

Result:
case intro.h.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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).carrier
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).carrier), gi X • x = t.hom.app X.obj x
cl : PointedGaloisObject F → Set G := fun X => gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
X : C
x✝ : IsGalois X
x : (F.obj X).carrier
s : G
hsmem : s • x = x
hg : gi { obj := X, pt := x, isGalois := ⋯ } • s ∈ c
⊢ gi { obj := X, pt := x, isGalois := ⋯ } • x = t.hom.app X x