simp [fintypeEquivFin]
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ fintypeEquivFin true = 1
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ cast ⋯ ((List.Nodup.getEquivOfForallMemList (sortedUniv Bool) ⋯ ⋯).symm true) = 1