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

State before:
α : Type u_1
inst : FinDenumerable α
⊢ Function.Injective encode_fin
Tactic:
intro x y
State after:
α : Type u_1
inst : FinDenumerable α
x y : α
⊢ encode_fin x = encode_fin y → x = y

State before:
α : Type u_1
inst : FinDenumerable α
x y : α
⊢ encode_fin x = encode_fin y → x = y
Tactic:
simp [Fin.ext_iff, encode_fin]
State after:
no goals