simp [Encodable.fintypeEquivFin, Fin.cast_eq_cast',
  Fin.encodable, List.Nodup.getEquivOfForallMemList,
  Encodable.sortedUniv, Encodable.encode']
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ ↑(Fin.cast ⋯ (fintypeEquivFin i)) = ↑i
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ List.indexOf i (Finset.sort (encode ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ) = ↑i