case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq α
s : Multiset α
x : α
⊢ x ∈ Finite.toFinset (_ : Set.Finite {x | x ∈ s}) ↔ x ∈ toFinset s
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq α
s : Multiset α
⊢ Finite.toFinset (_ : Set.Finite {x | x ∈ s}) = toFinset s
ext x
no goals
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq α
s : Multiset α
x : α
⊢ x ∈ Finite.toFinset (_ : Set.Finite {x | x ∈ s}) ↔ x ∈ toFinset s
simp