α : Type u_1
β : Type ?u.420411
γ : Type ?u.420414
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ ↑(List.filter (fun b_1 => decide (b_1 = b)) l) = replicate (List.count b l) b
α : Type u_1
β : Type ?u.420411
γ : Type ?u.420414
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ filter (fun x => x = b) (Quotient.mk (isSetoid α) l) = replicate (count b (Quotient.mk (isSetoid α) l)) b
simp only [quot_mk_to_coe, coe_filter, mem_coe, coe_count]
no goals
α : Type u_1
β : Type ?u.420411
γ : Type ?u.420414
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ ↑(List.filter (fun b_1 => decide (b_1 = b)) l) = replicate (List.count b l) b
rw [List.filter_eq' l b, coe_replicate]