-- Mathlib/CategoryTheory/Galois/EssSurj.lean
/-- If `X` is a finite discrete `G`-set, it can be written as the finite disjoint union
of quotients of the form `G ⧸ Uᵢ` for open subgroups `(Uᵢ)`. Note that this
is simply the decomposition into orbits. -/
lemma has_decomp_quotients (X : Action FintypeCat G)
    [TopologicalSpace X.V] [DiscreteTopology X.V] [ContinuousSMul G X.V] :
    ∃ (ι : Type) (_ : Finite ι) (f : ι → OpenSubgroup (G)),
      Nonempty ((∐ fun i ↦ G ⧸ₐ (f i).toSubgroup) ≅ X)

Proof state:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul G X.V.carrier
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝ : (i : ι) → TopologicalSpace (f i).V.carrier := fun i => ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.carrier
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.carrier → G × X.V.carrier := fun p => (p.1, r.hom p.2)
q : G × X.V.carrier → X.V.carrier := fun p => X.ρ p.1 p.2
q' : G × (f i).V.carrier → (f i).V.carrier := fun p => (f i).ρ p.1 p.2
heq : q ∘ r'' = r.hom ∘ q'
hrinj : Function.Injective r.hom
t₁ : TopologicalSpace (G × (f i).V.carrier) := inferInstance
⊢ Continuous fun p => p.1 • p.2

Tactic:
show @Continuous _ _ _ ⊥ q'

Result:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul G X.V.carrier
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝ : (i : ι) → TopologicalSpace (f i).V.carrier := fun i => ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.carrier
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.carrier → G × X.V.carrier := fun p => (p.1, r.hom p.2)
q : G × X.V.carrier → X.V.carrier := fun p => X.ρ p.1 p.2
q' : G × (f i).V.carrier → (f i).V.carrier := fun p => (f i).ρ p.1 p.2
heq : q ∘ r'' = r.hom ∘ q'
hrinj : Function.Injective r.hom
t₁ : TopologicalSpace (G × (f i).V.carrier) := inferInstance
⊢ Continuous q'

Proof state:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul G X.V.carrier
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝ : (i : ι) → TopologicalSpace (f i).V.carrier := fun i => ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.carrier
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.carrier → G × X.V.carrier := fun p => (p.1, r.hom p.2)
q : G × X.V.carrier → X.V.carrier := fun p => X.ρ p.1 p.2
q' : G × (f i).V.carrier → (f i).V.carrier := fun p => (f i).ρ p.1 p.2
heq : q ∘ r'' = r.hom ∘ q'
hrinj : Function.Injective r.hom
⊢ Continuous fun p => p.1 • p.2

Tactic:
let t₁ : TopologicalSpace (G × (f i).V) := inferInstance

Result:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul G X.V.carrier
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝ : (i : ι) → TopologicalSpace (f i).V.carrier := fun i => ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.carrier
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.carrier → G × X.V.carrier := fun p => (p.1, r.hom p.2)
q : G × X.V.carrier → X.V.carrier := fun p => X.ρ p.1 p.2
q' : G × (f i).V.carrier → (f i).V.carrier := fun p => (f i).ρ p.1 p.2
heq : q ∘ r'' = r.hom ∘ q'
hrinj : Function.Injective r.hom
t₁ : TopologicalSpace (G × (f i).V.carrier) := inferInstance
⊢ Continuous fun p => p.1 • p.2

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul G X.V.carrier
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝¹ : (i : ι) → TopologicalSpace (f i).V.carrier := fun i => ⊥
this✝ : ∀ (i : ι), DiscreteTopology (f i).V.carrier
this : ∀ (i : ι), ContinuousSMul G (f i).V.carrier
g : ι → OpenSubgroup G
ui : ∀ (i : ι), Nonempty (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(g i))))
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i => Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)

Tactic:
exact ⟨ι, hf, g, ⟨(Sigma.mapIso (fun i ↦ (ui i).some)).symm ≪≫ u⟩⟩

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul G X.V.carrier
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝² : (i : ι) → TopologicalSpace (f i).V.carrier := fun i => ⊥
this✝¹ : ∀ (i : ι), DiscreteTopology (f i).V.carrier
this✝ : ∀ (i : ι), ContinuousSMul G (f i).V.carrier
i : ι
x : (f i).V.carrier
U : OpenSubgroup G := { toSubgroup := MulAction.stabilizer G x, isOpen' := ⋯ }
this : Fintype (G ⧸ MulAction.stabilizer G x) := CategoryTheory.PreGaloisCategory.fintypeQuotient U
⊢ ∃ U, Nonempty (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑U)))

Tactic:
exact ⟨U, ⟨FintypeCat.isoQuotientStabilizerOfIsConnected (f i) x⟩⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul G X.V.carrier
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝ : (i : ι) → TopologicalSpace (f i).V.carrier := fun i => ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.carrier
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
⊢ Continuous fun p => p.1 • p.2

Tactic:
let r'' (p : G × (f i).V) : G × X.V := (p.1, r.hom p.2)

Result:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul G X.V.carrier
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝ : (i : ι) → TopologicalSpace (f i).V.carrier := fun i => ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.carrier
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.carrier → G × X.V.carrier := fun p => (p.1, r.hom p.2)
⊢ Continuous fun p => p.1 • p.2