awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Basic
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 A : C
inst_3 : Nonempty.{w + 1} (F.obj X).obj
inst_4 : IsConnected.{u₁, u₂} A
f : X ⟶ A
this : Epi f
⊢ Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 X)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))

Tactic:
surjective_on_fiber_of_epi F f

Premises used: CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi
-- Module: Mathlib.CategoryTheory.Galois.Basic
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 A : C
inst_3 : Nonempty.{w + 1} (F.obj X).obj
inst_4 : IsConnected.{u₁, u₂} A
f : X ⟶ A
this : Epi f
⊢ Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 X)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))

Tactic:
exact surjective_on_fiber_of_epi F f

Premises used: CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
ι : Type u_1
inst_3 : Finite ι
X : ι → C
inst_4 : ∀ (i : ι), Nonempty.{w + 1} (F.obj (X i)).obj
intro : ∀ (val : Fintype ι), Nonempty.{w + 1} (F.obj (piObj.{u_1, u₂, u₁} X)).obj
⊢ Nonempty.{w + 1} (F.obj (piObj.{u_1, u₂, u₁} X)).obj

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
ι : Type u_1
inst_3 : Finite ι
X : ι → C
inst_4 : ∀ (i : ι), Nonempty.{w + 1} (F.obj (X i)).obj
val : Fintype ι
f : (i : ι) → FintypeCat := fun (i : ι) ↦ F.obj (X i)
i : F.obj (piObj.{u_1, u₂, u₁} X) ≅ ∏ᶜ f := PreservesProduct.iso F X
⊢ Nonempty.{w + 1} (F.obj (piObj.{u_1, u₂, u₁} X)).obj

Tactic:
Nonempty.elim inferInstance fun x : (∏ᶜ f : FintypeCat.{w}) ↦ ⟨i.inv x⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Nonempty.elim, inferInstance, Nonempty.intro, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
ι : Type u_1
inst_3 : Finite ι
X : ι → C
inst_4 : ∀ (i : ι), Nonempty.{w + 1} (F.obj (X i)).obj
val : Fintype ι
f : (i : ι) → FintypeCat := fun (i : ι) ↦ F.obj (X i)
i : F.obj (piObj.{u_1, u₂, u₁} X) ≅ ∏ᶜ f := PreservesProduct.iso F X
⊢ Nonempty.{w + 1} (F.obj (piObj.{u_1, u₂, u₁} X)).obj

Tactic:
exact Nonempty.elim inferInstance fun x : (∏ᶜ f : FintypeCat.{w}) ↦ ⟨i.inv x⟩
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
apply :
  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)
⊢ IsIso (F.map f)

Tactic:
apply (ConcreteCategory.isIso_iff_bijective (F.map f)).mpr

Premises used: Iff.mpr, CategoryTheory.Functor.map, CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
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))
⊢ 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)

Tactic:
apply (Fintype.bijective_iff_injective_and_card (F.map f)).mpr

Premises used: Iff.mpr, CategoryTheory.ConcreteCategory.hom, Fintype.bijective_iff_injective_and_card, CategoryTheory.Functor.map, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.Basic
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))

Tactic:
⟨injective_of_mono_of_preservesPullback (F.map f), ?_⟩

Premises used: CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback, CategoryTheory.Functor.map, And.intro
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
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))
⊢ 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:
refine ⟨injective_of_mono_of_preservesPullback (F.map f), ?_⟩
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
⊢ 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:
simp only [← Nat.card_eq_fintype_card, h]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.CategoryTheory.Galois.Basic
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.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]
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
this : IsIso (F.map f)
⊢ IsIso f

Tactic:
isIso_of_reflects_iso f F

Premises used: CategoryTheory.isIso_of_reflects_iso
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
this : IsIso (F.map f)
⊢ IsIso f

Tactic:
exact isIso_of_reflects_iso f F

Premises used: CategoryTheory.isIso_of_reflects_iso
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
by_contra : ∀ (hlt : ¬Nat.card.{w} (F.obj X).obj < Nat.card.{w} (F.obj Y).obj), False
⊢ Nat.card.{w} (F.obj X).obj < Nat.card.{w} (F.obj Y).obj

Tactic:
by_contra hlt
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
apply : IsIso f
⊢ False

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
apply : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj
⊢ IsIso f

Tactic:
apply isIso_of_mono_of_eq_card_fiber F f

Premises used: CategoryTheory.PreGaloisCategory.isIso_of_mono_of_eq_card_fiber
-- Module: Mathlib.CategoryTheory.Galois.Basic
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 Y).obj ≤ Nat.card.{w} (F.obj X).obj

Tactic:
simp only [not_lt] at hlt

Premises used: not_lt
-- Module: Mathlib.CategoryTheory.Galois.Basic
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 Y).obj ≤ Nat.card.{w} (F.obj X).obj
⊢ Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj

Tactic:
Nat.le_antisymm
    (Nat.card_le_card_of_injective (F.map f) (injective_of_mono_of_preservesPullback (F.map f))) hlt

Premises used: Nat.card_le_card_of_injective, CategoryTheory.ConcreteCategory.hom, CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback, CategoryTheory.Functor.map, Nat.le_antisymm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.Basic
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 Y).obj ≤ Nat.card.{w} (F.obj X).obj
⊢ Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj

Tactic:
exact Nat.le_antisymm
    (Nat.card_le_card_of_injective (F.map f) (injective_of_mono_of_preservesPullback (F.map f))) hlt

Premises used: Nat.card_le_card_of_injective, CategoryTheory.ConcreteCategory.hom, CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback, CategoryTheory.Functor.map, Nat.le_antisymm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.Basic
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

Tactic:
Nonempty.elim ?_ h

Premises used: Nonempty.elim
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
refine : Nonempty (IsInitial.{u₂, u₁} X)
⊢ False

Tactic:
refine Nonempty.elim ?_ h

Premises used: Nonempty.elim
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
rw : IsEmpty.{w + 1} (F.obj X).obj
⊢ Nonempty (IsInitial.{u₂, u₁} X)

Tactic:
rw [initial_iff_fiber_empty F]

Premises used: CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
⊢ IsEmpty.{w + 1} (F.obj X).obj

Tactic:
Finite.card_eq_zero_iff.mp hzero

Premises used: Finite.card_eq_zero_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
⊢ IsEmpty.{w + 1} (F.obj X).obj

Tactic:
exact Finite.card_eq_zero_iff.mp hzero

Premises used: Finite.card_eq_zero_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Galois.Basic
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)))
rw : Nat.card.{w} (F.obj (coprod.{u₂, u₁} X Y)).obj = Nat.card.{w} ((F.obj X).obj ⊕ (F.obj Y).obj)
⊢ 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

Tactic:
rw [← Nat.card_sum]

Premises used: Nat.card_sum
-- Module: Mathlib.CategoryTheory.Galois.Basic
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 ⊕ (F.obj Y).obj)

Tactic:
Nat.card_eq_of_bijective e.toFun (Equiv.bijective e)

Premises used: Equiv.bijective, Equiv.toFun, Nat.card_eq_of_bijective
-- Module: Mathlib.CategoryTheory.Galois.Basic
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 ⊕ (F.obj Y).obj)

Tactic:
exact Nat.card_eq_of_bijective e.toFun (Equiv.bijective e)

Premises used: Equiv.bijective, Equiv.toFun, Nat.card_eq_of_bijective
-- Module: Mathlib.CategoryTheory.Galois.Basic
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)
f : (A ⟶ X) → (F.obj X).obj
⊢ Nat.card.{u₂} (A ⟶ X) ≤ Nat.card.{w} (F.obj X).obj

Tactic:
apply Nat.card_le_card_of_injective

Premises used: Nat.card_le_card_of_injective
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
⊢ 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:
evaluation_injective_of_isConnected F A X (Classical.arbitrary _)

Premises used: CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected, Classical.arbitrary
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
⊢ Nonempty.{w + 1} (F.obj A).obj

Tactic:
have h : Nonempty (F.obj A) := inferInstance
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
obtain : ∀ (a : (F.obj A).obj), Nat.card.{u₂} (Aut A) ≤ Nat.card.{w} (F.obj A).obj
⊢ Nat.card.{u₂} (Aut A) ≤ Nat.card.{w} (F.obj A).obj

Tactic:
obtain ⟨a⟩ := h
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
f : Aut A → (F.obj A).obj
⊢ Nat.card.{u₂} (Aut A) ≤ Nat.card.{w} (F.obj A).obj

Tactic:
apply Nat.card_le_card_of_injective

Premises used: Nat.card_le_card_of_injective
-- Module: Mathlib.CategoryTheory.Galois.Basic
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
⊢ 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:
evaluation_aut_injective_of_isConnected _ _ a

Premises used: CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected