α : Type u_1
β : Type ?u.2011
γ : Type ?u.2014
r : α → α → Prop
s✝ t : Multiset α
a : α
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ List.Nodup _l ↔ ∀ (a : α), List.count a _l ≤ 1
α : Type u_1
β : Type ?u.2011
γ : Type ?u.2014
r : α → α → Prop
s✝ t : Multiset α
a : α
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ Nodup (Quot.mk Setoid.r _l) ↔ ∀ (a : α), count a (Quot.mk Setoid.r _l) ≤ 1
simp only [quot_mk_to_coe'', coe_nodup, mem_coe, coe_count]
no goals
α : Type u_1
β : Type ?u.2011
γ : Type ?u.2014
r : α → α → Prop
s✝ t : Multiset α
a : α
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ List.Nodup _l ↔ ∀ (a : α), List.count a _l ≤ 1
apply List.nodup_iff_count_le_one