-- 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:
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 => ⊥
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i => Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)

Tactic:
haveI (i : ι) : DiscreteTopology (f i).V := ⟨rfl⟩

Result:
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
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i => Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ 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'
⊢ Continuous fun p => p.1 • p.2

Tactic:
have hrinj : Function.Injective r.hom :=
  (ConcreteCategory.mono_iff_injective_of_preservesPullback r).mp <| mono_comp _ _

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
⊢ Continuous fun p => p.1 • p.2

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)
⊢ Continuous fun p => p.1 • p.2

Tactic:
let q (p : G × X.V) : X.V := X.ρ p.1 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)
q : G × X.V.carrier → X.V.carrier := fun p => X.ρ p.1 p.2
⊢ Continuous fun p => p.1 • p.2

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 : ι
⊢ Continuous fun p => p.1 • p.2

Tactic:
let r : f i ⟶ X := Sigma.ι f i ≫ u.hom

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
⊢ Continuous fun p => p.1 • p.2

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
⊢ TopologicalSpace.induced r.hom inferInstance ≤ ⊥

Tactic:
exact fun s _ ↦ ⟨r.hom '' s, ⟨isOpen_discrete (r.hom '' s), Set.preimage_image_eq s hrinj⟩⟩

Result:
no goals