X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fintype.card (Fin (len X + 1)) = Fintype.card (Fin (len Y + 1))
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ X = Y
suffices Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1)) by
  ext
  simpa
case f
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fin (len X + 1) ≃ Fin (len Y + 1)
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fintype.card (Fin (len X + 1)) = Fintype.card (Fin (len Y + 1))
apply Fintype.card_congr
no goals
case f
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fin (len X + 1) ≃ Fin (len Y + 1)
exact Equiv.ulift.symm.trans
  (((skeletalFunctor.{0} ⋙ forget NonemptyFinLinOrdCat).mapIso I).toEquiv.trans Equiv.ulift)
case a
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (len X + 1)) = Fintype.card (Fin (len Y + 1))
⊢ len X = len Y
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (len X + 1)) = Fintype.card (Fin (len Y + 1))
⊢ X = Y
ext
no goals
case a
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (len X + 1)) = Fintype.card (Fin (len Y + 1))
⊢ len X = len Y
simpa