have ⟨ _, h ⟩ := fin_preimage_exists n
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
w✝ : α
h : Encodable.encode w✝ = ↑n
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n