α : Type u_1
β : Type ?u.176256
γ : Type ?u.176259
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ a ::ₘ erase s a ∩ erase t a
α : Type u_1
β : Type ?u.176256
γ : Type ?u.176259
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ s ∩ t
rw [← cons_erase h₁, cons_inter_of_pos _ h₂]
no goals
α : Type u_1
β : Type ?u.176256
γ : Type ?u.176259
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ a ::ₘ erase s a ∩ erase t a
apply mem_cons_self