case a
α : Type u_1
β : Type ?u.399939
γ : Type ?u.399942
inst✝ : DecidableEq α
s t : List α
a✝ : α
⊢ count a✝ (↑s ∩ ↑t) = count a✝ ↑(List.bagInter s t)
α : Type u_1
β : Type ?u.399939
γ : Type ?u.399942
inst✝ : DecidableEq α
s t : List α
⊢ ↑s ∩ ↑t = ↑(List.bagInter s t)
ext
no goals
case a
α : Type u_1
β : Type ?u.399939
γ : Type ?u.399942
inst✝ : DecidableEq α
s t : List α
a✝ : α
⊢ count a✝ (↑s ∩ ↑t) = count a✝ ↑(List.bagInter s t)
simp