∀ (α : Type u_1) [inst : Fintype α] [inst_1 : CategoryTheory.SmallCategory α] [inst_2 : CategoryTheory.FinCategory α]
  {X Y Z : CategoryTheory.FinCategory.AsType α} (f : Fin (Fintype.card (X ⟶ Y))) (g : Fin (Fintype.card (Y ⟶ Z))),
  CategoryTheory.CategoryStruct.comp f g =
    (Fintype.equivFin (X ⟶ Z))
      (CategoryTheory.CategoryStruct.comp ((Fintype.equivFin (X ⟶ Y)).symm f) ((Fintype.equivFin (Y ⟶ Z)).symm g))