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

Tactic:
have (i : ι) : ContinuousSMul G (f i).V := ContinuousSMul.mk <| by
  let r : f i ⟶ X := Sigma.ι f i ≫ u.hom
  let r'' (p : G × (f i).V) : G × X.V := (p.1, r.hom p.2)
  let q (p : G × X.V) : X.V := X.ρ p.1 p.2
  let q' (p : G × (f i).V) : (f i).V := (f i).ρ p.1 p.2
  have heq : q ∘ r'' = r.hom ∘ q' := by
    ext (p : G × (f i).V)
    exact (congr_fun (r.comm p.1) p.2).symm
  have hrinj : Function.Injective r.hom :=
    (ConcreteCategory.mono_iff_injective_of_preservesPullback r).mp <| mono_comp _ _
  let t₁ : TopologicalSpace (G × (f i).V) := inferInstance
  show @Continuous _ _ _ ⊥ q'
  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⟩⟩
  rw [← this, continuous_induced_rng, ← heq]
  exact Continuous.comp continuous_smul (by fun_prop)

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
⊢ ∃ ι, ∃ (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'
hrinj : Function.Injective r.hom
t₁ : TopologicalSpace (G × (f i).V.carrier) := inferInstance
this : TopologicalSpace.induced r.hom inferInstance = ⊥
⊢ Continuous r''

Tactic:
fun_prop

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

Tactic:
exact Continuous.comp continuous_smul (by fun_prop)

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' := ⋯ }
⊢ ∃ U, Nonempty (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑U)))

Tactic:
letI : Fintype (G ⧸ MulAction.stabilizer (G) x) := fintypeQuotient U

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

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

Tactic:
letI (i : ι) : TopologicalSpace (f i).V := ⊥

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