case a
α : Type u_1
β : Type ?u.451772
γ : Type ?u.451775
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
a✝ : α
⊢ a✝ ∈ toFinset (s ∪ t) ↔ a✝ ∈ toFinset s ∪ toFinset t
α : Type u_1
β : Type ?u.451772
γ : Type ?u.451775
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
⊢ toFinset (s ∪ t) = toFinset s ∪ toFinset t
ext
no goals
case a
α : Type u_1
β : Type ?u.451772
γ : Type ?u.451775
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
a✝ : α
⊢ a✝ ∈ toFinset (s ∪ t) ↔ a✝ ∈ toFinset s ∪ toFinset t
simp