α : Type u_1
β : Type ?u.168188
γ : Type ?u.168191
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u ∪ t
α : Type u_1
β : Type ?u.168188
γ : Type ?u.168191
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u
rw [← eq_union_left h₂]
no goals
α : Type u_1
β : Type ?u.168188
γ : Type ?u.168191
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u ∪ t
exact union_le_union_right h₁ t