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

Tactic:
exact hgi ⟨X, x, inferInstance⟩ x

Result:
no goals

Proof state:
case h
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
s : Finset (PointedGaloisObject F)
gs : G
hgs : ∀ (i : { x // x ∈ s }) (x : (F.obj (↑i).obj).carrier), gs • x = t.hom.app (↑i).obj x
X : PointedGaloisObject F
hXmem : X ∈ s
⊢ gs ∈ cl X

Tactic:
rw [mem_leftCoset_iff, SetLike.mem_coe, MulAction.mem_stabilizer_iff, mul_smul,
  hgs ⟨X, hXmem⟩, ← hgi X, inv_smul_smul]

Result:
no goals

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
g : G
hg : g ∈ c
X : C
x✝ : IsGalois X
x : (F.obj X).carrier
⊢ g ∈ gi { obj := X, pt := x, isGalois := ⋯ } • ↑(MulAction.stabilizer G x)

Tactic:
simp only [Set.mem_iInter, c] at hg

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)
c : Set G := ⋂ i, cl i
g : G
X : C
x✝ : IsGalois X
x : (F.obj X).carrier
hg : ∀ (i : PointedGaloisObject F), g ∈ cl i
⊢ g ∈ gi { obj := X, pt := x, isGalois := ⋯ } • ↑(MulAction.stabilizer G x)

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

Tactic:
intro X

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
X : PointedGaloisObject F
⊢ IsClosed (cl X)

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
⊢ c.Nonempty

Tactic:
rw [← Set.univ_inter c]

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)
c : Set G := ⋂ i, cl i
⊢ (Set.univ ∩ c).Nonempty