p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ List.length (List.filter (fun b => decide (p b)) (List.range n)) = card (filter p (range n))
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = card (filter p (range n))
rw [count, List.countp_eq_length_filter]
no goals
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ List.length (List.filter (fun b => decide (p b)) (List.range n)) = card (filter p (range n))
rfl