-- 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
this : TopologicalSpace.induced r.hom inferInstance = ⊥
⊢ Continuous q'

Tactic:
rw [← this, continuous_induced_rng, ← heq]

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
this : TopologicalSpace.induced r.hom inferInstance = ⊥
⊢ Continuous (q ∘ r'')

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 q'

Tactic:
have : TopologicalSpace.induced r.hom inferInstance = ⊥ := by
  rw [← le_bot_iff]
  exact fun s _ ↦ ⟨r.hom '' s, ⟨isOpen_discrete (r.hom '' s), Set.preimage_image_eq s hrinj⟩⟩

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
this : TopologicalSpace.induced r.hom inferInstance = ⊥
⊢ Continuous q'