no goals
α : Type u_1
inst✝ : DecidableEq α
s✝ s t u : Multiset α
⊢ ndunion 0 t ≤ u ↔ 0 ⊆ u ∧ t ≤ u
simp [zero_ndunion]
no goals
α : Type u_1
inst✝ : DecidableEq α
s✝ s t u : Multiset α
x✝¹ : α
x✝ : Multiset α
h : ndunion x✝ t ≤ u ↔ x✝ ⊆ u ∧ t ≤ u
⊢ ndunion (x✝¹ ::ₘ x✝) t ≤ u ↔ x✝¹ ::ₘ x✝ ⊆ u ∧ t ≤ u
simp only [cons_ndunion, mem_ndunion, ndinsert_le, and_comm, cons_subset, and_left_comm, h,
and_assoc]