no goals
α✝ : Type ?u.13820
β : Type ?u.13823
γ : Type ?u.13826
α : Type u_1
inst✝ : Fintype α
l : List α
h : Nodup l
⊢ length l ≤ Fintype.card α
classical exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ
no goals
α✝ : Type ?u.13820
β : Type ?u.13823
γ : Type ?u.13826
α : Type u_1
inst✝ : Fintype α
l : List α
h : Nodup l
⊢ length l ≤ Fintype.card α
exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ