no goals
α : Type u_1
β : Type ?u.174218
γ : Type ?u.174221
inst✝ : DecidableEq α
s✝¹ t✝ u : Multiset α
a✝ b : α
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t : Multiset α), s ∩ t ≤ t
t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t
simpa [h] using cons_le_cons a (IH (t.erase a))
no goals
α : Type u_1
β : Type ?u.174218
γ : Type ?u.174221
inst✝ : DecidableEq α
s✝¹ t✝ u : Multiset α
a✝ b : α
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t : Multiset α), s ∩ t ≤ t
t : Multiset α
h : ¬a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t
simp [h, IH]