α : Type u_1
β : Type ?u.411904
γ : Type ?u.411907
inst✝ : DecidableEq α
s t : Multiset α
al : ∀ (a : α), count a s ≤ count a t
⊢ s ≤ s ∪ t
α : Type u_1
β : Type ?u.411904
γ : Type ?u.411907
inst✝ : DecidableEq α
s t : Multiset α
al : ∀ (a : α), count a s ≤ count a t
⊢ s ≤ t
rw [← (ext.2 fun a => by simp [max_eq_right (al a)] : s ∪ t = t)]
no goals
α : Type u_1
β : Type ?u.411904
γ : Type ?u.411907
inst✝ : DecidableEq α
s t : Multiset α
al : ∀ (a : α), count a s ≤ count a t
⊢ s ≤ s ∪ t
apply le_union_left
no goals
α : Type u_1
β : Type ?u.411904
γ : Type ?u.411907
inst✝ : DecidableEq α
s t : Multiset α
al : ∀ (a : α), count a s ≤ count a t
a : α
⊢ count a (s ∪ t) = count a t
simp [max_eq_right (al a)]