awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
⊢ FiberFunctor.{u₁, u₂, u₂} (GaloisCategory.getFiberFunctor C)

Tactic:
Classical.choice <| Classical.choose_spec (@GaloisCategory.hasFiberFunctor C _ _)

Premises used: Classical.choice, Classical.choose_spec, CategoryTheory.GaloisCategory.hasFiberFunctor
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A X : C
inst_2 : IsConnected.{u₁, u₂} A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
obtain : ∀ (a : (F.obj A).obj), Finite.{u₂ + 1} (A ⟶ X)
⊢ Finite.{u₂ + 1} (A ⟶ X)

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Premises used: CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A X : C
inst_2 : IsConnected.{u₁, u₂} A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
apply :
  Function.Injective (β := (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
⊢ Finite.{u₂ + 1} (A ⟶ X)

Tactic:
apply Finite.of_injective (fun f ↦ F.map f a)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, DFunLike.coe, Finite.of_injective
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A X : C
inst_2 : IsConnected.{u₁, u₂} A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ Function.Injective (β := (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

Tactic:
evaluation_injective_of_isConnected F A X a

Premises used: CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A X : C
inst_2 : IsConnected.{u₁, u₂} A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ Function.Injective (β := (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

Tactic:
exact evaluation_injective_of_isConnected F A X a

Premises used: CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A : C
inst_2 : IsConnected.{u₁, u₂} A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
obtain : ∀ (a : (F.obj A).obj), Finite.{u₂ + 1} (Aut A)
⊢ Finite.{u₂ + 1} (Aut A)

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Premises used: CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A : C
inst_2 : IsConnected.{u₁, u₂} A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
apply :
  Function.Injective (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) fun (f : Aut 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.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a
⊢ Finite.{u₂ + 1} (Aut A)

Tactic:
apply Finite.of_injective (fun f ↦ F.map f.hom a)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, DFunLike.coe, Finite.of_injective
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A : C
inst_2 : IsConnected.{u₁, u₂} A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ Function.Injective (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) fun (f : Aut 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.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a

Tactic:
evaluation_aut_injective_of_isConnected F A a

Premises used: CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A : C
inst_2 : IsConnected.{u₁, u₂} A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ Function.Injective (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) fun (f : Aut 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.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a

Tactic:
exact evaluation_aut_injective_of_isConnected F A a

Premises used: CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ MonoCoprod.{u₂, u₁} C

Tactic:
MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono F

Premises used: CategoryTheory.Limits.MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ MonoCoprod.{u₂, u₁} C

Tactic:
exact MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono F

Premises used: CategoryTheory.Limits.MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
inst_1 : IsConnected.{u₁, u₂} X
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
⟨Unit, fun _ ↦ X, fun _ ↦ 𝟙 X, Cofan.IsColimit.mk _ (fun s ↦ s.inj ()), ?_⟩

Premises used: Unit.unit, CategoryTheory.Limits.Cofan.IsColimit.mk, CategoryTheory.CategoryStruct.id, Unit, CategoryTheory.Limits.Cofan.inj, Exists.intro
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
inst_1 : IsConnected.{u₁, u₂} X
refine : (∀ (i : Unit), IsConnected.{u₁, u₂} (C := C) ((fun (x : Unit) ↦ X) i)) ∧ Finite Unit
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
refine ⟨Unit, fun _ ↦ X, fun _ ↦ 𝟙 X, Cofan.IsColimit.mk _ (fun s ↦ s.inj ()), ?_⟩
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
inst_1 : IsConnected.{u₁, u₂} X
⊢ (∀ (i : Unit), IsConnected.{u₁, u₂} (C := C) ((fun (x : Unit) ↦ X) i)) ∧ Finite Unit

Tactic:
⟨fun _ ↦ inferInstance, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
inst_1 : IsConnected.{u₁, u₂} X
⊢ (∀ (i : Unit), IsConnected.{u₁, u₂} (C := C) ((fun (x : Unit) ↦ X) i)) ∧ Finite Unit

Tactic:
exact ⟨fun _ ↦ inferInstance, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
h : IsInitial.{u₂, u₁} X
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
⟨Empty, fun _ ↦ X, fun _ ↦ 𝟙 X, ?_⟩

Premises used: CategoryTheory.CategoryStruct.id, Empty, Exists.intro
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
h : IsInitial.{u₂, u₁} X
refine :
  ∃ (x :
    IsColimit.{0, u₂, 0, u₁} (J := Discrete Empty) (F := Discrete.functor fun (x : Empty) ↦ X)
      (Cofan.mk X fun (x : Empty) ↦ 𝟙 X)),
    (∀ (i : Empty), IsConnected.{u₁, u₂} (C := C) ((fun (x : Empty) ↦ X) i)) ∧ Finite Empty
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι

Tactic:
refine ⟨Empty, fun _ ↦ X, fun _ ↦ 𝟙 X, ?_⟩
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
h : IsInitial.{u₂, u₁} X
s : Cofan.{0, u₂, u₁} (C := C) fun (x : Empty) ↦ X
⊢ ∀ (j : Empty),
    CategoryStruct.comp (Y :=
        Cocone.pt.{0, u₂, 0, u₁} (J := Discrete Empty) (F := Discrete.functor fun (x : Empty) ↦ X)
          (Cofan.mk X fun (x : Empty) ↦ 𝟙 X))
        (Cofan.inj.{0, u₂, u₁} (f := fun (x : Empty) ↦ X) (Cofan.mk X fun (x : Empty) ↦ 𝟙 X) j)
        ((fun (s : Cofan.{0, u₂, u₁} (C := C) fun (x : Empty) ↦ X) ↦ (h.to s.pt : X ⟶ s.pt)) s) =
      s.inj j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
h : IsInitial.{u₂, u₁} X
h₁ : (∀ (i : Empty), IsConnected.{u₁, u₂} (C := C) ((fun (x : Empty) ↦ X) i)) ∧ Finite Empty
⊢ ∃ (x :
    IsColimit.{0, u₂, 0, u₁} (J := Discrete Empty) (F := Discrete.functor fun (x : Empty) ↦ X)
      (Cofan.mk X fun (x : Empty) ↦ 𝟙 X)),
    (∀ (i : Empty), IsConnected.{u₁, u₂} (C := C) ((fun (x : Empty) ↦ X) i)) ∧ Finite Empty

Tactic:
use Cofan.IsColimit.mk _ (fun s ↦ IsInitial.to h s.pt) (fun s ↦ by simp)
    (fun s m _ ↦ IsInitial.hom_ext h m _)

Premises used: CategoryTheory.Limits.Cofan.IsColimit.mk
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
h : IsInitial.{u₂, u₁} X
⊢ ∀ (i : Empty), IsConnected.{u₁, u₂} (C := C) ((fun (x : Empty) ↦ X) i)

Tactic:
simp only [IsEmpty.forall_iff]

Premises used: IsEmpty.forall_iff
-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
h : IsInitial.{u₂, u₁} X
⊢ (∀ (i : Empty), IsConnected.{u₁, u₂} (C := C) ((fun (x : Empty) ↦ X) i)) ∧ Finite Empty

Tactic:
exact ⟨by simp only [IsEmpty.forall_iff], inferInstance⟩
-- 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 : ℕ
ind :
  ∀ (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),
    n = 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),
    n = 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 ι

Tactic:
induction n using Nat.strongRecOn with | _ n hi
-- 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
pos :
  ∀ (h : IsConnected.{u₁, u₂} X),
    ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
      (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
neg :
  ∀ (h : ¬IsConnected.{u₁, u₂} X),
    ∃ (ι : 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:
by_cases h : IsConnected X

Premises used: CategoryTheory.PreGaloisCategory.IsConnected
-- 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
⊢ ∃ (ι : 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_conn X

Premises used: _private.0.CategoryTheory.PreGaloisCategory.has_decomp_connected_components_aux_conn
-- 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
⊢ ∃ (ι : 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_conn X

Premises used: _private.0.CategoryTheory.PreGaloisCategory.has_decomp_connected_components_aux_conn
-- 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
pos :
  ∀ (nhi : ∀ (a : IsInitial.{u₂, u₁} X), False),
    ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
      (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
neg :
  ∀ (nhi : ¬∀ (a : IsInitial.{u₂, u₁} X), False),
    ∃ (ι : 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:
by_cases nhi : IsInitial X → False
-- 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
pos :
  ∀ (Y : C) (v : Y ⟶ X) (hni : ∀ (a : IsInitial.{u₂, u₁} Y), False) (hvmono : Mono v) (hvnoiso : ¬IsIso v),
    ∃ (ι : 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 ⟨Y, v, hni, hvmono, hvnoiso⟩ :=
      has_non_trivial_subobject_of_not_isConnected_of_not_initial X h nhi

Premises used: CategoryTheory.PreGaloisCategory.has_non_trivial_subobject_of_not_isConnected_of_not_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 :
  ∀ 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
pos :
  ∀ (Z : C) (u : Z ⟶ X) (c : IsColimit (BinaryCofan.mk v u)),
    ∃ (ι : 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 ⟨Z, u, ⟨c⟩⟩ := PreGaloisCategory.monoInducesIsoOnDirectSummand v

Premises used: CategoryTheory.PreGaloisCategory.monoInducesIsoOnDirectSummand
-- 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 }
rw : Nat.card.{w} (F.obj Y).obj < Nat.card.{w} (F.obj X).obj
⊢ Nat.card.{w} (F.obj Y).obj < n

Tactic:
rw [hn]
-- 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 }
⊢ Nat.card.{w} (F.obj Y).obj < Nat.card.{w} (F.obj X).obj

Tactic:
lt_card_fiber_of_mono_of_notIso F v hvnoiso

Premises used: CategoryTheory.PreGaloisCategory.lt_card_fiber_of_mono_of_notIso
-- 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 }
⊢ Nat.card.{w} (F.obj Y).obj < Nat.card.{w} (F.obj X).obj

Tactic:
exact lt_card_fiber_of_mono_of_notIso F v hvnoiso

Premises used: CategoryTheory.PreGaloisCategory.lt_card_fiber_of_mono_of_notIso
-- 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 }
⊢ Nat.card.{w} (F.obj Y).obj < n

Tactic:
have hn1 : Nat.card (F.obj Y) < n := by
      rw [hn]
      exact lt_card_fiber_of_mono_of_notIso F v hvnoiso