apply Option.isSome_iff_exists.2
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Option.isSome (Encodable.decode ↑n) = true
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∃ a, Encodable.decode ↑n = some a