awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X)))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map u) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X)))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X)))
    (mkSelfProdFib F X : (F.obj (selfProd F X)).obj)
h2 : IsConnected.{u₁, u₂} A
h3 : Mono u
x : (F.obj X).obj
⊢ (fun (f : A ⟶ X) ↦
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
            a :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)))
      (u ≫ Pi.π (fun (x : (F.obj X).obj) ↦ X) x) =
    x

Tactic:
(selfProdProj_fiber h1) x

Premises used: _private.0.CategoryTheory.PreGaloisCategory.selfProdProj_fiber, _private.0.CategoryTheory.PreGaloisCategory.selfProdProj
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X)))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map u) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X)))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X)))
    (mkSelfProdFib F X : (F.obj (selfProd F X)).obj)
h2 : IsConnected.{u₁, u₂} A
h3 : Mono u
x : (F.obj X).obj
⊢ (fun (f : A ⟶ X) ↦
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
            a :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)))
      (u ≫ Pi.π (fun (x : (F.obj X).obj) ↦ X) x) =
    x

Tactic:
exact (selfProdProj_fiber h1) x

Premises used: _private.0.CategoryTheory.PreGaloisCategory.selfProdProj_fiber
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
x : (F.obj X).obj
obtain :
  ∀ (A : C) (a : (F.obj A).obj) (h1 : IsGalois.{u₁, u₂} A)
    (h2 :
      Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        fun (f : A ⟶ X) ↦
        (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (F.map f) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          a),
    ∃ (A : C) (f : A ⟶ X) (a : (F.obj A).obj),
      IsGalois.{u₁, u₂} A ∧
        (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
            a =
          x
⊢ ∃ (A : C) (f : A ⟶ X) (a : (F.obj A).obj),
    IsGalois.{u₁, u₂} A ∧
      (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (F.map f) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          a =
        x

Tactic:
obtain ⟨A, a, h1, h2⟩ := exists_galois_representative F X

Premises used: CategoryTheory.PreGaloisCategory.exists_galois_representative
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
x : (F.obj X).obj
A : C
a : (F.obj A).obj
h1 : IsGalois.{u₁, u₂} A
h2 :
  Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    fun (f : A ⟶ X) ↦
    (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a
f : A ⟶ X
hf :
  (fun (f : A ⟶ X) ↦
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
            a :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)))
      f =
    x
⊢ ∃ (A : C) (f : A ⟶ X) (a : (F.obj A).obj),
    IsGalois.{u₁, u₂} A ∧
      (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (F.map f) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          a =
        x

Tactic:
⟨A, f, a, h1, hf⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
x : (F.obj X).obj
A : C
a : (F.obj A).obj
h1 : IsGalois.{u₁, u₂} A
h2 :
  Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    fun (f : A ⟶ X) ↦
    (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a
f : A ⟶ X
hf :
  (fun (f : A ⟶ X) ↦
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
            a :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)))
      f =
    x
⊢ ∃ (A : C) (f : A ⟶ X) (a : (F.obj A).obj),
    IsGalois.{u₁, u₂} A ∧
      (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (F.map f) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          a =
        x

Tactic:
exact ⟨A, f, a, h1, hf⟩
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
h : Nonempty.{w + 1} (F.obj X).obj
obtain : ∀ (x : (F.obj X).obj), ∃ (A : C) (x : A ⟶ X), IsGalois.{u₁, u₂} A
⊢ ∃ (A : C) (x : A ⟶ X), IsGalois.{u₁, u₂} A

Tactic:
obtain ⟨x⟩ := h
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
x : (F.obj X).obj
obtain :
  ∀ (A : C) (f : A ⟶ X) (a : (F.obj A).obj) (h1 : IsGalois.{u₁, u₂} A),
    (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (F.map f) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          a =
        x →
      ∃ (A : C) (x : A ⟶ X), IsGalois.{u₁, u₂} A
⊢ ∃ (A : C) (x : A ⟶ X), IsGalois.{u₁, u₂} A

Tactic:
obtain ⟨A, f, a, h1, _⟩ := exists_hom_from_galois_of_fiber F X x

Premises used: CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
x : (F.obj X).obj
A : C
f : A ⟶ X
a : (F.obj A).obj
h1 : IsGalois.{u₁, u₂} A
right :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a =
    x
⊢ ∃ (A : C) (x : A ⟶ X), IsGalois.{u₁, u₂} A

Tactic:
⟨A, f, h1⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
x : (F.obj X).obj
A : C
f : A ⟶ X
a : (F.obj A).obj
h1 : IsGalois.{u₁, u₂} A
right :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a =
    x
⊢ ∃ (A : C) (x : A ⟶ X), IsGalois.{u₁, u₂} A

Tactic:
exact ⟨A, f, h1⟩
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
inst_3 : IsConnected.{u₁, u₂} X
⊢ ∃ (A : C) (x : A ⟶ X), IsGalois.{u₁, u₂} A

Tactic:
exists_hom_from_galois_of_fiber_nonempty F X inferInstance

Premises used: inferInstance, CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber_nonempty
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
G : Functor.{u₂, w, u₁, w + 1} C FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], t.app X = s.app X
w :
  ∀ (X : C) (x : (F.obj X).obj),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
      ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (t.app X) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
      ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (s.app X) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
⊢ t = s

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
obtain :
  ∀ (ι : Type) (hf : Finite ι) (f : ι → Action FintypeCat G) (u : ∐ f ≅ X) (hc : ∀ (i : ι), IsConnected (f i)),
    ∃ (ι : Type) (x : Finite ι) (f : ι → OpenSubgroup G),
      Nonempty.{u_1 + 1}
        ((∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑(f i) : Subgroup G)))) ≅ X)
⊢ ∃ (ι : Type) (x : Finite ι) (f : ι → OpenSubgroup G),
    Nonempty.{u_1 + 1}
      ((∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ (↑(f i) : Subgroup G)))) ≅ X)

Tactic:
obtain ⟨ι, hf, f, u, hc⟩ := has_decomp_connected_components' X

Premises used: CategoryTheory.PreGaloisCategory.has_decomp_connected_components'
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
⊢ ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj

Tactic:
haveI (i : ι) : DiscreteTopology (f i).V := ⟨rfl⟩
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this_1 : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
this : ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : (p : G × (f i).V.obj) → G × X.V.obj :=
  fun (p : G × (f i).V.obj) ↦
    (p.1,
      (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ r.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
        p.2)
q : (p : G × X.V.obj) → X.V.obj :=
  fun (p : G × X.V.obj) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((X.ρ : (a : G) → End X.V) p.1)) :
        (a : (fun (X : Type u_1) ↦ X) X.V.obj) → (fun (X : Type u_1) ↦ X) X.V.obj)
      p.2
q' : (p : G × (f i).V.obj) → (f i).V.obj :=
  fun (p : G × (f i).V.obj) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) (((f i).ρ : (a : G) → End (f i).V) p.1)) :
        (a : (fun (X : Type u_1) ↦ X) (f i).V.obj) → (fun (X : Type u_1) ↦ X) (f i).V.obj)
      p.2
p : G × (f i).V.obj
⊢ (q ∘ r'') p =
    ((⇑(@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ r.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) ∘
        q')
      p

Tactic:
(ConcreteCategory.congr_hom (r.comm p.1) p.2).symm

Premises used: Prod.fst, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, Prod.snd, Action.Hom.comm