no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : a ∈ l₁
⊢ count a (List.dedup l₁) = count a (List.dedup l₂)
simp [nodup_dedup, h, p.subset h]
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : ¬a ∈ l₁
⊢ count a (List.dedup l₁) = count a (List.dedup l₂)
simp [h, mt p.mem_iff.2 h]