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

State before:
α : Type u_1
inst✝ : FinDenumerable α
⊢ Function.LeftInverse decode_fin encode_fin
Tactic:
intro _
State after:
α : Type u_1
inst✝ : FinDenumerable α
x✝ : α
⊢ decode_fin (encode_fin x✝) = x✝

State before:
α : Type u_1
inst✝ : FinDenumerable α
x✝ : α
⊢ decode_fin (encode_fin x✝) = x✝
Tactic:
simp [encode_fin, decode_fin]
State after:
no goals