no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Multiset α
⊢ Set.Finite {x | x ∈ s}
classical simpa only [← Multiset.mem_toFinset] using s.toFinset.finite_toSet
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Multiset α
⊢ Set.Finite {x | x ∈ s}
simpa only [← Multiset.mem_toFinset] using s.toFinset.finite_toSet