case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s ∪ t + s ∩ t ≤ s + t

case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s + t ≤ s ∪ t + s ∩ t
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s ∪ t + s ∩ t = s + t
apply _root_.le_antisymm
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s + s ∩ t ∪ (t + s ∩ t) ≤ s + t
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s ∪ t + s ∩ t ≤ s + t
rw [union_add_distrib]
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ t + s ∩ t ≤ s + t
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s + s ∩ t ∪ (t + s ∩ t) ≤ s + t
refine' union_le (add_le_add_left (inter_le_right _ _) _) _
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s ∩ t + t ≤ s + t
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ t + s ∩ t ≤ s + t
rw [add_comm]
no goals
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s ∩ t + t ≤ s + t
exact add_le_add_right (inter_le_left _ _) _
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s + t ≤ s ∪ t + s ∩ t
rw [add_comm, add_inter_distrib]
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ t + s ≤ s ∪ t + t
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)
refine' le_inter (add_le_add_right (le_union_right _ _) _) _
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s + t ≤ s ∪ t + t
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ t + s ≤ s ∪ t + t
rw [add_comm]
no goals
case a
α : Type u_1
β : Type ?u.190902
γ : Type ?u.190905
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s + t ≤ s ∪ t + t
exact add_le_add_right (le_union_left _ _) _