lifting `α ↪ α` to `α ≃ α` in the presence of `fintype α`?

Stream: Is there code for X?

[Scott Morrison]

Do we have

def function.embedding.equiv_of_fintype_endomorphism {α : Type*} [fintype α] (e : α ↪ α) : α ≃ α := ...

(I don't mind if it is noncomputable particularly; presumably computability would further require [decidable_eq α].)

[Scott Morrison]

I came up with the rather unpleasant

noncomputable def function.embedding.equiv_of_fintype_endomorphism {α : Type*} [fintype α] (e : α ↪ α) : α ≃ α :=
begin
  apply function.embedding.equiv_of_surjective e _,
  apply (fintype.injective_iff_surjective_of_equiv (equiv.refl α)).mp _,
  exact function.embedding.inj e,
end

from the pieces I could find already available, but I'm hoping there's something better available.

[Bhavik Mehta]

Not clear if it's better but I came up with

noncomputable def function.embedding.equiv_of_fintype_endomorphism {α : Type*} [fintype α] (e : α ↪ α) : α ≃ α :=
begin
  apply equiv.of_bijective,
  rw ← fintype.injective_iff_bijective,
  exact e.2
end

[Bhavik Mehta]

Term mode version:

noncomputable def function.embedding.equiv_of_fintype_endomorphism {α : Type*} [fintype α] (e : α ↪ α) : α ≃ α :=
equiv.of_bijective (fintype.injective_iff_bijective.1 e.2)

[Scott Morrison]

Thanks, that's perfect.