α : Type u_1
β : Type ?u.395888
γ : Type ?u.395891
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ List.count a _l ↔ replicate n a ≤ ↑_l
α : Type u_1
β : Type ?u.395888
γ : Type ?u.395891
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ count a (Quot.mk Setoid.r _l) ↔ replicate n a ≤ Quot.mk Setoid.r _l
simp only [quot_mk_to_coe'', mem_coe, coe_count]
no goals
α : Type u_1
β : Type ?u.395888
γ : Type ?u.395891
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ List.count a _l ↔ replicate n a ≤ ↑_l
exact le_count_iff_replicate_sublist.trans replicate_le_coe.symm