no goals
α✝ : Type ?u.54720
β : Type ?u.54723
γ : Type ?u.54726
α : Type u_1
inst✝ : Fintype α
e : α ↪ α
⊢ map e univ = univ
rw [← e.equiv_of_fintype_self_embedding_to_embedding, univ_map_equiv_to_embedding]