α : Type u_1
β : Type ?u.479712
γ : Type ?u.479715
s : Finset α
⊢ Nodup s.val
α : Type u_1
β : Type ?u.479712
γ : Type ?u.479715
s : Finset α
⊢ List.Nodup (toList s)
rw [toList, ← Multiset.coe_nodup, Multiset.coe_toList]
no goals
α : Type u_1
β : Type ?u.479712
γ : Type ?u.479715
s : Finset α
⊢ Nodup s.val
exact s.nodup