have tmp := Equiv.ofLeftInverse encode_fin (fun _ => inst.decode_fin) (fun _ => encodek_fin_left_inverse)
α : Type u_1
inst : FinDenumerable α
⊢ α ≃ Fin (Fintype.card α)
α : Type u_1
inst : FinDenumerable α
tmp : α ≃ ↑(Set.range encode_fin)
⊢ α ≃ Fin (Fintype.card α)