α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
p : α → Bool
l₁ l₂ : List α
s : l₁ ~ l₂
⊢ length (List.filter p l₁) = length (List.filter p l₂)
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
p : α → Bool
l₁ l₂ : List α
s : l₁ ~ l₂
⊢ countp p l₁ = countp p l₂
rw [countp_eq_length_filter, countp_eq_length_filter]
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
p : α → Bool
l₁ l₂ : List α
s : l₁ ~ l₂
⊢ length (List.filter p l₁) = length (List.filter p l₂)
exact (s.filter _).length_eq