Theorem: FinDenumerable.decode_fin_eq_option_get (FormalSystems/Preliminaries/FinDenumerable.lean)

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Option.get (Encodable.decode ↑n) ⋯ = decode_fin n
Tactic:
simp [decode_fin]
State after:
no goals