Mapping finset.univ along an equiv gives finset.univ

Stream: Is there code for X?

[Eric Wieser]

This feels like it should exist somewhere:

lemma finset.univ_map_equiv {α β : Type*} [fintype α] [fintype β] (f : α ≃ β) :
  (finset.univ : finset α).map f.to_embedding = (finset.univ : finset β) :=
sorry

[Eric Wieser]

Ah, library_search was just slow - docs#finset.univ_map_equiv_to_embedding