case a
α : Type u_1
β : Type ?u.13180
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
a : α
⊢ count a (dedup (n • s)) = count a (dedup s)
α : Type u_1
β : Type ?u.13180
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
⊢ dedup (n • s) = dedup s
ext a
no goals
case a
α : Type u_1
β : Type ?u.13180
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
a : α
⊢ count a (dedup (n • s)) = count a (dedup s)
by_cases h : a ∈ s <;> simp [h, h0]