Is there a simple way to lift Finset (Fin n) to Finset Nat?

Stream: new members

[Kevin Cheung]

I have the following:

import Mathlib.Tactic.LibrarySearch
import Mathlib.Data.Fintype.Basic

def set4 : Finset (Fin 4) := {0, 1, 2, 3}
def set4' : Finset ℕ := {0, 1, 2, 3}

I wanted to prove that set4 and set4' are equal. After some experimenting, I came upon the following:

example : set4' = Finset.map ⟨Fin.val, Fin.val_injective⟩ set4 := rfl

But the statement of the proposition seems a bit verbose. Is there a cleaner way to express that set4 and set4' are equal?

[Yaël Dillies]

No, you found the correct spelling

[Kevin Cheung]

Thank you.

[Jireh Loreaux]

There's no bundling of Fin.val as an embedding?

[Jireh Loreaux]

docs#Fin.valEmbedding

[Kevin Cheung]

Thank you. So the following works:

example : set4' = Finset.map Fin.valEmbedding set4 := rfl

Are there tricks to finding these things?

[Jireh Loreaux]

You can use loogle:

@loogle ⊢ Fin ?n ↪ ℕ

[loogle]

:search: Fin.valEmbedding