α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
l : List α
a : α
⊢ True ∧ ∀ (b : α), b ∈ l ∧ b = a → b = a
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
l : List α
a : α
⊢ filter (fun x => x == a) l = replicate (count a l) a
simp only [count, countp_eq_length_filter, eq_replicate, mem_filter, beq_iff_eq]
no goals
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
l : List α
a : α
⊢ True ∧ ∀ (b : α), b ∈ l ∧ b = a → b = a
exact ⟨trivial, fun _ h => h.2⟩