α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (List.map (↑Equiv.symm) (List.finRange (card α)))
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (toList α)
simp [toList]
no goals
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (List.map (↑Equiv.symm) (List.finRange (card α)))
apply List.Nodup.map <;> [apply Equiv.injective; apply List.nodup_finRange]