awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
F : Functor.{v₁, v, u₁, u} D C
inst_3 : Nonempty D
⊢ IsCofiltered (SmallCofilteredIntermediate F)

Tactic:
{ (inferInstance : IsCofilteredOrEmpty _) with
    nonempty := Nonempty.map (factoring F).obj inferInstance }

Premises used: inferInstance, CategoryTheory.IsCofiltered.mk
-- Module: Mathlib.CategoryTheory.FinCategory.Basic
Goal:
α : Type u_1
inst : Finite α
⊢ Finite.{u_1 + 1} (Discrete α)

Tactic:
Finite.of_equiv α discreteEquiv.symm

Premises used: Finite.of_equiv, Equiv.symm, CategoryTheory.discreteEquiv
-- Module: Mathlib.CategoryTheory.FinCategory.Basic
Goal:
α : Type u_1
X Y : Discrete α
⊢ Fintype (X ⟶ Y)

Tactic:
apply ULift.fintype

Premises used: ULift.fintype
-- Module: Mathlib.CategoryTheory.FinCategory.Basic
Goal:
α : Type u_1
X Y : Discrete α
⊢ Fintype (X ⟶ Y)

Tactic:
classical
  apply ULift.fintype

Premises used: ULift.fintype
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
⊢ Finite.{u_1 + 1} X.obj

Tactic:
X.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
⊢ incl.Full

Tactic:
ObjectProperty.full_ι _

Premises used: CategoryTheory.ObjectProperty.full_ι
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
⊢ incl.Faithful

Tactic:
ObjectProperty.faithful_ι _

Premises used: CategoryTheory.ObjectProperty.faithful_ι
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
⊢ Functor.Full
    (forget FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))

Tactic:
inferInstanceAs <| FintypeCat.incl.Full

Premises used: _private.0.FintypeCat.instFullForgetFunObjFinite._proof_1
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
x : X.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))
          _ _ _ (𝟙 X : X ⟶ X) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X)
      x =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y Z : FintypeCat
f : X ⟶ Y
g : Y ⟶ Z
x : X.obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Z)
    ((@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 ≫ g) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Z)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Z)
    ((@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))
            _ _ _ g :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Z)
        ((@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 :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
            x :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
f : X ⟶ Y
x : X.obj
⊢ Eq (α := (fun (X : Type u_1) ↦ X) Y.obj)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom (F := ObjectProperty.FullSubcategory.obj)) :
          (a : (fun (X : Type u_1) ↦ X) X.obj) → (fun (X : Type u_1) ↦ X) Y.obj)
        x :
      (fun (X : Type u_1) ↦ X) 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 :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
f : X ≅ Y
x : X.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.inv :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.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.hom :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y) =
    x

Tactic:
ConcreteCategory.congr_hom f.hom_inv_id x

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
f : X ≅ Y
y : 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.hom :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.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.inv :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X)
          y :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) =
    y

Tactic:
ConcreteCategory.congr_hom f.inv_hom_id y

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
f g : X ⟶ Y
h :
  ∀ (x : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.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 :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.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))
              _ _ _ g :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ h

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
f : X.obj → Y.obj
x : X.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))
          _ _ _ (homMk f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
      x =
    f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
⊢ 𝟙 X.obj = ↾id

Tactic:
rfl

Premises used: TypeCat.Fun.id, rfl
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y Z : FintypeCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ f.hom (F := ObjectProperty.FullSubcategory.obj) ≫ g.hom (F := ObjectProperty.FullSubcategory.obj) =
    ↾Function.comp (β := (fun (X : Type u_1) ↦ X) Y.obj)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (g.hom (F := ObjectProperty.FullSubcategory.obj))) :
          (a : (fun (X : Type u_1) ↦ X) Y.obj) → (fun (X : Type u_1) ↦ X) Z.obj)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom (F := ObjectProperty.FullSubcategory.obj))) :
          (a : (fun (X : Type u_1) ↦ X) X.obj) → (fun (X : Type u_1) ↦ X) Y.obj)

Tactic:
rfl

Premises used: TypeCat.Fun.comp, rfl
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
f : X.obj → X.obj
mp : homMk f = 𝟙 X → f = id
mpr : f = id → homMk f = 𝟙 X
⊢ homMk f = 𝟙 X ↔ f = id

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
f : X.obj → X.obj
h : homMk f = 𝟙 X
mp : ∀ (x : X.obj), f x = id x
⊢ f = id

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
f : X.obj → X.obj
h : homMk f = 𝟙 X
x : X.obj
⊢ f x = id x

Tactic:
ConcreteCategory.congr_hom h x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
f : X.obj → X.obj
h : homMk f = 𝟙 X
x : X.obj
⊢ f x = id x

Tactic:
exact ConcreteCategory.congr_hom h x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
⊢ homMk id = 𝟙 X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h : X.obj → Z.obj
mp : homMk h = homMk f ≫ homMk g → h = g ∘ f
mpr : h = g ∘ f → homMk h = homMk f ≫ homMk g
⊢ homMk h = homMk f ≫ homMk g ↔ h = g ∘ f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h_1 : X.obj → Z.obj
h : homMk h_1 = homMk f ≫ homMk g
mp : ∀ (x : X.obj), h_1 x = (g ∘ f) x
⊢ h_1 = g ∘ f

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h_1 : X.obj → Z.obj
h : homMk h_1 = homMk f ≫ homMk g
x : X.obj
⊢ h_1 x = (g ∘ f) x

Tactic:
ConcreteCategory.congr_hom h x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h_1 : X.obj → Z.obj
h : homMk h_1 = homMk f ≫ homMk g
x : X.obj
⊢ h_1 x = (g ∘ f) x

Tactic:
exact ConcreteCategory.congr_hom h x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
⊢ homMk (g ∘ f) = homMk f ≫ homMk g

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
⊢ Finite.{u_1 + 1} (X ⟶ Y)

Tactic:
Finite.of_equiv _ (show (X ⟶ Y) ≃ (X → Y) from
    InducedCategory.homEquiv.trans TypeCat.homEquiv).symm

Premises used: Finite.of_equiv, CategoryTheory.InducedCategory.homEquiv, Equiv.trans, TypeCat.homEquiv, Equiv.symm
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
⊢ Finite.{u_1 + 1} (X ≅ Y)

Tactic:
Finite.of_injective _ (fun _ _ h ↦ Iso.ext h)

Premises used: CategoryTheory.Iso.ext, Finite.of_injective
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
⊢ Finite.{u_1 + 1} (Aut X)

Tactic:
inferInstanceAs <| Finite (X ≅ X)

Premises used: _private.0.FintypeCat.instFiniteAut._proof_1
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : Skeleton
⊢ X.len = Y.len → X = Y

Tactic:
ULift.ext _ _

Premises used: ULift.ext, FintypeCat.Skeleton.len, FintypeCat.Skeleton
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
rw : ULift.down.{u, 0} (h.inv (h.hom { down := a : ULift.{u, 0} (Fin X.len) })) = a
⊢ ULift.down.{u, 0}
      (h.inv
        { down := (fun (x : Fin X.len) ↦ (h.hom { down := x : ULift.{u, 0} (Fin X.len) }).down) a :
          ULift.{u, 0} (Fin Y.len) }) =
    a

Tactic:
rw [ULift.up_down]

Premises used: ULift.up_down
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
change : ULift.down.{u, 0} ((h.hom ≫ h.inv) { down := a : ULift.{u, 0} (Fin X.len) }) = a
⊢ ULift.down.{u, 0} (h.inv (h.hom { down := a : ULift.{u, 0} (Fin X.len) })) = a

Tactic:
change ((h.hom ≫ h.inv) _).down = _

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, ULift.down, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
simp : ULift.down.{u, 0} (𝟙 X { down := a }) = a
⊢ ULift.down.{u, 0} ((h.hom ≫ h.inv) { down := a : ULift.{u, 0} (Fin X.len) }) = a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ ULift.down.{u, 0} (𝟙 X { down := a }) = a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
rw : ULift.down.{u, 0} (h.hom (h.inv { down := a : ULift.{u, 0} (Fin Y.len) })) = a
⊢ ULift.down.{u, 0}
      (h.hom
        { down := (fun (x : Fin Y.len) ↦ (h.inv { down := x : ULift.{u, 0} (Fin Y.len) }).down) a :
          ULift.{u, 0} (Fin X.len) }) =
    a

Tactic:
rw [ULift.up_down]

Premises used: ULift.up_down
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
change : ULift.down.{u, 0} ((h.inv ≫ h.hom) { down := a : ULift.{u, 0} (Fin Y.len) }) = a
⊢ ULift.down.{u, 0} (h.hom (h.inv { down := a : ULift.{u, 0} (Fin Y.len) })) = a

Tactic:
change ((h.inv ≫ h.hom) _).down = _

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, ULift.down, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
simp : ULift.down.{u, 0} (𝟙 Y { down := a }) = a
⊢ ULift.down.{u, 0} ((h.inv ≫ h.hom) { down := a : ULift.{u, 0} (Fin Y.len) }) = a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ ULift.down.{u, 0} (𝟙 Y { down := a }) = a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : Skeleton
a₁ a₂ : X ⟶ Y
h : incl.map a₁ = incl.map a₂
⊢ a₁ = a₂

Tactic:
simpa using TypeCat.homEquiv.symm.injective (InducedCategory.homEquiv.symm.injective h)

Premises used: CategoryTheory.InducedCategory.homEquiv, TypeCat.homEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
⊢ incl.EssSurj

Tactic:
Functor.EssSurj.mk fun X =>
    letI := X.fintype
    let F := Fintype.equivFin X
    ⟨mk (Fintype.card X),
      Nonempty.intro
        { hom := homMk (F.symm ∘ ULift.down)
          inv := homMk (ULift.up ∘ F) }⟩

Premises used: FintypeCat.Skeleton.mk, Function.comp, Fintype.card, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Iso.mk, CategoryTheory.Functor.EssSurj.mk, Nonempty.intro, Fintype.equivFin, Exists.intro, Equiv.symm, ULift.up, DFunLike.coe, ULift.down, FintypeCat.homMk, FintypeCat.fintype
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
n : ℕ
⊢ Finset.card (α := Fin n) Finset.univ = n

Tactic:
Finset.card_fin n

Premises used: Finset.card_fin
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
n : ℕ
h : Fintype.card.{u_1} (incl.obj (mk n)).obj = Finset.card (α := Fin n) Finset.univ
⊢ Fintype.card.{u_1} (incl.obj (mk n)).obj = n

Tactic:
convert! Finset.card_fin n

Premises used: Finset.card_fin
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
n : ℕ
h : Fintype.card.{u_1} (ULift.{u_1, 0} (Fin n)) = Fintype.card (Fin n)
⊢ Fintype.card.{u_1} (incl.obj (mk n)).obj = Finset.card (α := Fin n) Finset.univ

Tactic:
dsimp [incl, mk, len]

Premises used: FintypeCat.Skeleton.mk, FintypeCat.Skeleton.incl, FintypeCat.Skeleton.len
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
n : ℕ
⊢ Fintype.card.{u_1} (ULift.{u_1, 0} (Fin n)) = Fintype.card (Fin n)

Tactic:
(Fintype.ofEquiv_card Equiv.ulift).symm

Premises used: Equiv.ulift, Fintype.ofEquiv_card, Eq.symm
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
n : ℕ
⊢ Fintype.card.{u_1} (ULift.{u_1, 0} (Fin n)) = Fintype.card (Fin n)

Tactic:
convert! (Fintype.ofEquiv_card Equiv.ulift).symm

Premises used: Equiv.ulift, Fintype.ofEquiv_card, Eq.symm
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
⊢ Skeleton.incl.IsEquivalence

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj X).obj
⊢ Eq (α := 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 :
          (a : X.obj) → Y.obj)
        ((Equiv.symm (Fintype.equivFin X.obj) : (a : Fin (Fintype.card X.obj)) → X.obj) x.down : X.obj) :
      Y.obj)
    ((Equiv.symm (Fintype.equivFin Y.obj) : (a : Fin (Fintype.card Y.obj)) → Y.obj)
        (ULift.down.{v, 0}
          ((ULift.up ∘
              Function.comp (β := Y.obj) (⇑(Fintype.equivFin Y.obj) : (a : Y.obj) → Fin (Fintype.card Y.obj))
                (Function.comp (β := X.obj)
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom (F := ObjectProperty.FullSubcategory.obj))) :
                    (a : X.obj) → Y.obj)
                  ((⇑(Equiv.symm (Fintype.equivFin X.obj)) : (a : Fin (Fintype.card X.obj)) → X.obj) ∘ ULift.down)))
            x)) :
      Y.obj)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
f : X ⟶ Y
⊢ uSwitch.map (uSwitch.map f) =
    Iso.hom
        ((equivEquivIso : (a : (uSwitch.obj (uSwitch.obj X)).obj ≃ X.obj) → uSwitch.obj (uSwitch.obj X) ≅ X)
          (Equiv.trans (uSwitch.obj X).uSwitchEquiv X.uSwitchEquiv)) ≫
      f ≫
        Iso.inv
          ((equivEquivIso : (a : (uSwitch.obj (uSwitch.obj Y)).obj ≃ Y.obj) → uSwitch.obj (uSwitch.obj Y) ≅ Y)
            (Equiv.trans (uSwitch.obj Y).uSwitchEquiv Y.uSwitchEquiv))

Tactic:
rfl

Premises used: TypeCat.Fun.comp, FintypeCat.homMk, rfl