α : Type u_1
β : Type ?u.156876
γ : Type ?u.156879
inst✝ : DecidableEq α
t u : Multiset α
a b : α
⊢ ∀ {s : Multiset α}, s - t ≤ u ↔ s ≤ u + t
α : Type u_1
β : Type ?u.156876
γ : Type ?u.156879
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
⊢ s - t ≤ u ↔ s ≤ u + t
revert s
no goals
α : Type u_1
β : Type ?u.156876
γ : Type ?u.156879
inst✝ : DecidableEq α
t u : Multiset α
a b : α
⊢ ∀ {s : Multiset α}, s - t ≤ u ↔ s ≤ u + t
exact @(Multiset.induction_on t (by simp [Multiset.sub_zero]) fun a t IH s => by
    simp [IH, erase_le_iff_le_cons])
no goals
α : Type u_1
β : Type ?u.156876
γ : Type ?u.156879
inst✝ : DecidableEq α
t u : Multiset α
a b : α
⊢ ∀ {s : Multiset α}, s - 0 ≤ u ↔ s ≤ u + 0
simp [Multiset.sub_zero]
no goals
α : Type u_1
β : Type ?u.156876
γ : Type ?u.156879
inst✝ : DecidableEq α
t✝ u : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s : Multiset α}, s - t ≤ u ↔ s ≤ u + t
s : Multiset α
⊢ s - a ::ₘ t ≤ u ↔ s ≤ u + a ::ₘ t
simp [IH, erase_le_iff_le_cons]