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
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)
he₂ : Finite ι₂
val : ι₁
⊢ IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ (Sum.inl val))

Tactic:
exact 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
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)
he₂ : Finite ι₂
val : ι₂
⊢ IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ (Sum.inr val))

Tactic:
hf₂ _

Premises used: Sum.elim
-- 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
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∀ (a : IsInitial.{u₂, u₁} X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial.{u₂, u₁} Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone.{0, 0, u₂, u₁} (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card.{w} (F.obj Y).obj < n
i : X ≅ coprod.{u₂, u₁} Y Z
hnn : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj + Nat.card.{w} (F.obj Z).obj
hn2 : Nat.card.{w} (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected.{u₁, u₂} (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected.{u₁, u₂} (f₂ i)
he₂ : Finite ι₂
val : ι₂
⊢ IsConnected.{u₁, u₂} (Sum.elim f₁ f₂ (Sum.inr val))

Tactic:
exact 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
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ¬∀ (a : IsInitial.{u₂, u₁} X), False
⊢ ∃ (x : IsInitial.{u₂, u₁} X), True

Tactic:
simp only [not_forall, not_false_eq_true] at nhi

Premises used: not_false_eq_true, Classical.not_forall
-- 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
n : ℕ
hi :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
nhi : ∃ (x : IsInitial.{u₂, u₁} X), True
neg :
  ∀ (hi : IsInitial.{u₂, u₁} X),
    True →
      ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
        (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
obtain ⟨hi⟩ := nhi
-- 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
n : ℕ
hi_1 :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
hi : IsInitial.{u₂, u₁} X
h_1 : True
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
has_decomp_connected_components_aux_initial X hi

Premises used: _private.0.CategoryTheory.PreGaloisCategory.has_decomp_connected_components_aux_initial
-- 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
n : ℕ
hi_1 :
  ∀ m < n,
    ∀ (X : C),
      m = Nat.card.{w} (F.obj X).obj →
        ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
          (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
X : C
hn : n = Nat.card.{w} (F.obj X).obj
h : ¬IsConnected.{u₁, u₂} X
hi : IsInitial.{u₂, u₁} X
h_1 : True
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
exact has_decomp_connected_components_aux_initial X hi

Premises used: _private.0.CategoryTheory.PreGaloisCategory.has_decomp_connected_components_aux_initial
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X : C
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
has_decomp_connected_components_aux F (Nat.card <| F.obj X) X rfl

Premises used: Nat.card, CategoryTheory.ObjectProperty.FullSubcategory.obj, _private.0.CategoryTheory.PreGaloisCategory.has_decomp_connected_components_aux, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X : C
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
exact has_decomp_connected_components_aux F (Nat.card <| F.obj X) X rfl

Premises used: Nat.card, CategoryTheory.ObjectProperty.FullSubcategory.obj, _private.0.CategoryTheory.PreGaloisCategory.has_decomp_connected_components_aux, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X : C
obtain :
  ∀ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (hl : IsColimit (Cofan.mk X g))
    (hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)) (hf : Finite ι),
    ∃ (ι : Type) (x : Finite ι) (f : ι → C) (x : sigmaObj.{0, u₂, u₁} f ≅ X), ∀ (i : ι), IsConnected.{u₁, u₂} (f i)
⊢ ∃ (ι : Type) (x : Finite ι) (f : ι → C) (x : sigmaObj.{0, u₂, u₁} f ≅ X), ∀ (i : ι), IsConnected.{u₁, u₂} (f i)

Tactic:
obtain ⟨ι, f, g, hl, hc, hf⟩ := has_decomp_connected_components X

Premises used: CategoryTheory.PreGaloisCategory.has_decomp_connected_components
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X : C
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)
hf : Finite ι
⊢ ∃ (ι : Type) (x : Finite ι) (f : ι → C) (x : sigmaObj.{0, u₂, u₁} f ≅ X), ∀ (i : ι), IsConnected.{u₁, u₂} (f i)

Tactic:
⟨ι, hf, f, colimit.isoColimitCocone ⟨Cofan.mk X g, hl⟩, hc⟩

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone, CategoryTheory.Limits.ColimitCocone.mk, Exists.intro, CategoryTheory.Limits.Cofan.mk
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X : C
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)
hf : Finite ι
⊢ ∃ (ι : Type) (x : Finite ι) (f : ι → C) (x : sigmaObj.{0, u₂, u₁} f ≅ X), ∀ (i : ι), IsConnected.{u₁, u₂} (f i)

Tactic:
exact ⟨ι, hf, f, colimit.isoColimitCocone ⟨Cofan.mk X g, hl⟩, hc⟩
-- 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 :
  ∀ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (hl : IsColimit (Cofan.mk X g))
    (hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)) (he : Finite ι),
    ∃ (Y : C) (i : Y ⟶ X) (y : (F.obj Y).obj),
      (@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 i) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
            y =
          x ∧
        IsConnected.{u₁, u₂} Y ∧ Mono i
⊢ ∃ (Y : C) (i : Y ⟶ X) (y : (F.obj Y).obj),
    (@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 i) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          y =
        x ∧
      IsConnected.{u₁, u₂} Y ∧ Mono i

Tactic:
obtain ⟨ι, f, g, hl, hc, he⟩ := has_decomp_connected_components X

Premises used: CategoryTheory.PreGaloisCategory.has_decomp_connected_components
-- 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
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)
he : Finite ι
s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
s' : IsColimit s := isColimitOfPreserves F hl
obtain :
  ∀ (j : ι)
    (z :
      ToType (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
        ObjectProperty.FullSubcategory.obj) ((Discrete.functor f ⋙ F).obj { as := j : Discrete ι }))
    (h :
      (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              ObjectProperty.FullSubcategory.obj
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _
              (s.ι.app { as := j } :
                (Discrete.functor f ⋙ F).obj { as := j : Discrete ι } ⟶
                  obj (obj (const (Discrete ι)) s.pt) { as := j : Discrete ι }) :
            (a : ((Discrete.functor f ⋙ F).obj { as := j }).obj) →
              (((const (Discrete ι)).obj s.pt).obj { as := j }).obj)
          z =
        x),
    ∃ (Y : C) (i : Y ⟶ X) (y : (F.obj Y).obj),
      (@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 i) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
            y =
          x ∧
        IsConnected.{u₁, u₂} Y ∧ Mono i
⊢ ∃ (Y : C) (i : Y ⟶ X) (y : (F.obj Y).obj),
    (@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 i) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          y =
        x ∧
      IsConnected.{u₁, u₂} Y ∧ Mono i

Tactic:
obtain ⟨⟨j⟩, z, h⟩ := Concrete.isColimit_exists_rep _ s' x

Premises used: CategoryTheory.Limits.Concrete.isColimit_exists_rep
-- 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
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)
he : Finite ι
s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
s' : IsColimit s := isColimitOfPreserves F hl
j : ι
z :
  ToType (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
    ObjectProperty.FullSubcategory.obj) ((Discrete.functor f ⋙ F).obj { as := j : Discrete ι })
h :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          ObjectProperty.FullSubcategory.obj
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _
          (s.ι.app { as := j } :
            (Discrete.functor f ⋙ F).obj { as := j : Discrete ι } ⟶
              obj (obj (const (Discrete ι)) s.pt) { as := j : Discrete ι }) :
        (a : ((Discrete.functor f ⋙ F).obj { as := j }).obj) → (((const (Discrete ι)).obj s.pt).obj { as := j }).obj)
      z =
    x
⊢ ∃ (Y : C) (i : Y ⟶ X) (y : (F.obj Y).obj),
    (@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 i) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          y =
        x ∧
      IsConnected.{u₁, u₂} Y ∧ Mono i

Tactic:
⟨f j, g j, z, ⟨?_, hc j, MonoCoprod.mono_inj _ (Cofan.mk X g) hl j⟩⟩

Premises used: CategoryTheory.Limits.MonoCoprod.mono_inj, And.intro, Exists.intro, CategoryTheory.Limits.Cofan.mk
-- 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
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)
he : Finite ι
s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
s' : IsColimit s := isColimitOfPreserves F hl
j : ι
z :
  ToType (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
    ObjectProperty.FullSubcategory.obj) ((Discrete.functor f ⋙ F).obj { as := j : Discrete ι })
h :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          ObjectProperty.FullSubcategory.obj
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _
          (s.ι.app { as := j } :
            (Discrete.functor f ⋙ F).obj { as := j : Discrete ι } ⟶
              obj (obj (const (Discrete ι)) s.pt) { as := j : Discrete ι }) :
        (a : ((Discrete.functor f ⋙ F).obj { as := j }).obj) → (((const (Discrete ι)).obj s.pt).obj { as := j }).obj)
      z =
    x
refine :
  (@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 (g j)) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (f j))) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      z =
    x
⊢ ∃ (Y : C) (i : Y ⟶ X) (y : (F.obj Y).obj),
    (@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 i) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          y =
        x ∧
      IsConnected.{u₁, u₂} Y ∧ Mono i

Tactic:
refine ⟨f j, g j, z, ⟨?_, hc j, MonoCoprod.mono_inj _ (Cofan.mk X g) hl j⟩⟩
-- 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
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected.{u₁, u₂} (f i)
he : Finite ι
s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
s' : IsColimit s := isColimitOfPreserves F hl
j : ι
z :
  ToType (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
    ObjectProperty.FullSubcategory.obj) ((Discrete.functor f ⋙ F).obj { as := j : Discrete ι })
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.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))
            _ _ _ (F.map (g j)) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (f j))) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            ObjectProperty.FullSubcategory.obj
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _
            (s.ι.app { as := j } :
              (Discrete.functor f ⋙ F).obj { as := j : Discrete ι } ⟶
                obj (obj (const (Discrete ι)) s.pt) { as := j : Discrete ι }) :
          (a : ((Discrete.functor f ⋙ F).obj { as := j }).obj) → (((const (Discrete ι)).obj s.pt).obj { as := j }).obj)
        z :
      (obj (obj (const (Discrete ι)) s.pt) { as := j : Discrete ι }).obj)

Tactic:
rfl