-- 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
this : ∀ (i : ι), ContinuousSMul G (f i).V.carrier
i : ι
⊢ ∃ U, Nonempty (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑U)))

Tactic:
obtain ⟨(x : (f i).V)⟩ := nonempty_fiber_of_isConnected (forget₂ _ _) (f i)

Result:
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, Nonempty (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑U)))

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
⊢ q ∘ r'' = r.hom ∘ q'

Tactic:
ext (p : G × (f i).V)

Result:
case h
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
p : G × (f i).V.carrier
⊢ (q ∘ r'') p = (r.hom ∘ q') p

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:
rw [← le_bot_iff]

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

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

Tactic:
choose g ui using this

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

Proof state:
case h
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
p : G × (f i).V.carrier
⊢ (q ∘ r'') p = (r.hom ∘ q') p

Tactic:
exact (congr_fun (r.comm p.1) p.2).symm

Result:
no goals