awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
inst_3 : Mono f
h : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj
⊢ Function.Bijective (α := (F.obj X).obj) (β := (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 f)) :
      (a : (F.obj X).obj) → (F.obj Y).obj)
have apply : Function.Injective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    (⇑(@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 X)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) ∧
  Fintype.card.{w} ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) =
    Fintype.card.{w} ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
Tactic: apply (Fintype.bijective_iff_injective_and_card (F.map f)).mpr
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
inst_3 : Mono f
h : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj
⊢ Function.Injective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) (β :=
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
      (⇑(@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 X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) ∧
    Fintype.card.{w} ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) =
      Fintype.card.{w} ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
have refine : Fintype.card.{w} ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) =
  Fintype.card.{w} ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
Tactic: refine ⟨injective_of_mono_of_preservesPullback (F.map f), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
inst_3 : Mono f
h : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj
⊢ IsIso f
have this : IsIso (F.map f)
Tactic: have : IsIso (F.map f) := by
    apply (ConcreteCategory.isIso_iff_bijective (F.map f)).mpr
    apply (Fintype.bijective_iff_injective_and_card (F.map f)).mpr
    refine ⟨injective_of_mono_of_preservesPullback (F.map f), ?_⟩
    simp only [← Nat.card_eq_fintype_card, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
inst_3 : Mono f
h : ¬IsIso f
⊢ Nat.card.{w} (F.obj X).obj < Nat.card.{w} (F.obj Y).obj
have by_contra : ∀ (hlt : ¬Nat.card.{w} (F.obj X).obj < Nat.card.{w} (F.obj Y).obj), False
Tactic: by_contra hlt
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
inst_3 : Mono f
h : ¬IsIso f
hlt : ¬Nat.card.{w} (F.obj X).obj < Nat.card.{w} (F.obj Y).obj
⊢ False
have apply : IsIso f
Tactic: apply h
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
inst_3 : Mono f
h : ¬IsIso f
hlt : ¬Nat.card.{w} (F.obj X).obj < Nat.card.{w} (F.obj Y).obj
⊢ IsIso f
have apply : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj
Tactic: apply isIso_of_mono_of_eq_card_fiber F f
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
inst_3 : Mono f
h : ¬IsIso f
hlt : ¬Nat.card.{w} (F.obj X).obj < Nat.card.{w} (F.obj Y).obj
⊢ Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj
have hlt₁ : Nat.card.{w} (F.obj Y).obj ≤ Nat.card.{w} (F.obj X).obj
Tactic: simp only [not_lt] at hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X : C
h : ∀ (a : IsInitial.{u₂, u₁} X), False
hzero : Nat.card.{w} (F.obj X).obj = 0
⊢ False
have refine : Nonempty (IsInitial.{u₂, u₁} X)
Tactic: refine Nonempty.elim ?_ h
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X : C
h : ∀ (a : IsInitial.{u₂, u₁} X), False
hzero : Nat.card.{w} (F.obj X).obj = 0
⊢ Nonempty (IsInitial.{u₂, u₁} X)
have rw : IsEmpty.{w + 1} (F.obj X).obj
Tactic: rw [initial_iff_fiber_empty F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
e : (F.obj (coprod.{u₂, u₁} X Y)).obj ≃ (F.obj X).obj ⊕ (F.obj Y).obj :=
  Iso.toEquiv
    (Iso.symm (PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y) ≪≫
      Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y)))
⊢ Nat.card.{w} (F.obj (coprod.{u₂, u₁} X Y)).obj = Nat.card.{w} (F.obj X).obj + Nat.card.{w} (F.obj Y).obj
have rw : Nat.card.{w} (F.obj (coprod.{u₂, u₁} X Y)).obj = Nat.card.{w} ((F.obj X).obj ⊕ (F.obj Y).obj)
Tactic: rw [← Nat.card_sum]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A X : C
inst_3 : IsConnected.{u₁, u₂} A
⊢ Nat.card.{u₂} (A ⟶ X) ≤ Nat.card.{w} (F.obj X).obj
have hf : Function.Injective.{u₂ + 1, w + 1} (β := (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))
    (Classical.arbitrary (F.obj A).obj)
Tactic: apply Nat.card_le_card_of_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A X : C
inst_3 : IsConnected.{u₁, u₂} A
hf :
  Function.Injective.{u₂ + 1, w + 1} (β := (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))
      (Classical.arbitrary (F.obj A).obj)
⊢ Nat.card.{u₂} (A ⟶ X) ≤ Nat.card.{w} (F.obj X).obj
have f : (A ⟶ X) → (F.obj X).obj
Tactic: apply Nat.card_le_card_of_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A : C
inst_3 : IsConnected.{u₁, u₂} A
⊢ Nat.card.{u₂} (Aut A) ≤ Nat.card.{w} (F.obj A).obj
have h : Nonempty.{w + 1} (F.obj A).obj
Tactic: have h : Nonempty (F.obj A) := inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A : C
inst_3 : IsConnected.{u₁, u₂} A
h : Nonempty.{w + 1} (F.obj A).obj
⊢ Nat.card.{u₂} (Aut A) ≤ Nat.card.{w} (F.obj A).obj
have obtain : ∀ (a : (F.obj A).obj), Nat.card.{u₂} (Aut A) ≤ Nat.card.{w} (F.obj A).obj
Tactic: obtain ⟨a⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
⊢ Nat.card.{u₂} (Aut A) ≤ Nat.card.{w} (F.obj A).obj
have hf : Function.Injective.{u₂ + 1, w + 1} (β := (F.obj A).obj) 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: apply Nat.card_le_card_of_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
hf :
  Function.Injective.{u₂ + 1, w + 1} (β := (F.obj A).obj) 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
⊢ Nat.card.{u₂} (Aut A) ≤ Nat.card.{w} (F.obj A).obj
have f : Aut A → (F.obj A).obj
Tactic: apply Nat.card_le_card_of_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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
⊢ Finite.{u₂ + 1} (A ⟶ X)
have obtain : ∀ (a : (F.obj A).obj), Finite.{u₂ + 1} (A ⟶ X)
Tactic: obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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
⊢ Finite.{u₂ + 1} (A ⟶ X)
have 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
Tactic: apply Finite.of_injective (fun f ↦ F.map f a)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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
⊢ Finite.{u₂ + 1} (Aut A)
have obtain : ∀ (a : (F.obj A).obj), Finite.{u₂ + 1} (Aut A)
Tactic: obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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
⊢ Finite.{u₂ + 1} (Aut A)
have 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
Tactic: apply Finite.of_injective (fun f ↦ F.map f.hom a)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 ι
have refine : (∀ (i : Unit), IsConnected.{u₁, u₂} (C := C) ((fun (x : Unit) ↦ X) i)) ∧ Finite Unit
Tactic: refine ⟨Unit, fun _ ↦ X, fun _ ↦ 𝟙 X, Cofan.IsColimit.mk _ (fun s ↦ s.inj ()), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 ι
have 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
Tactic: refine ⟨Empty, fun _ ↦ X, fun _ ↦ 𝟙 X, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
h : IsInitial.{u₂, u₁} X
⊢ ∃ (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
have h₁ : (∀ (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 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 : ℕ
⊢ ∀ (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 ι
have 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 ι
Tactic: induction n using Nat.strongRecOn with | _ n hi
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have 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 ι
Tactic: by_cases h : IsConnected X
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 ι
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have 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 ι
Tactic: by_cases h : IsConnected X
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 ι
have 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 ι
Tactic: by_cases nhi : IsInitial X → False
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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 ι
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have 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 ι
Tactic: by_cases nhi : IsInitial X → False
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have 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 ι
Tactic: obtain ⟨Y, v, hni, hvmono, hvnoiso⟩ :=
      has_non_trivial_subobject_of_not_isConnected_of_not_initial X h nhi
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Decomposition (goal)
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
⊢ ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (x : IsColimit (Cofan.mk X g)),
    (∀ (i : ι), IsConnected.{u₁, u₂} (f i)) ∧ Finite ι
have 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 ι
Tactic: obtain ⟨Z, u, ⟨c⟩⟩ := PreGaloisCategory.monoInducesIsoOnDirectSummand v