α : Type u_2
l✝ : List α
p✝ q : α → Bool
β : Type u_1
p : β → Bool
f : α → β
a : α
l : List α
⊢ (countp (p ∘ f) l + if p (f a) = true then 1 else 0) = countp (p ∘ f) l + if (p ∘ f) a = true then 1 else 0
α : Type u_2
l✝ : List α
p✝ q : α → Bool
β : Type u_1
p : β → Bool
f : α → β
a : α
l : List α
⊢ countp p (map f (a :: l)) = countp (p ∘ f) (a :: l)
rw [map_cons, countp_cons, countp_cons, countp_map p f l]
no goals
α : Type u_2
l✝ : List α
p✝ q : α → Bool
β : Type u_1
p : β → Bool
f : α → β
a : α
l : List α
⊢ (countp (p ∘ f) l + if p (f a) = true then 1 else 0) = countp (p ∘ f) l + if (p ∘ f) a = true then 1 else 0
rfl