α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t : Multiset α
a b : α
⊢ ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
h₁ : s ≤ t
h₂ : s ≤ u
⊢ s ≤ t ∩ u
revert s u
case refine_1
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t : Multiset α
a b : α
s u : Multiset α
h₁ : s ≤ 0
h₂ : s ≤ u
⊢ s ≤ 0 ∩ u

case refine_2
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
⊢ s ≤ (a ::ₘ t) ∩ u
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t : Multiset α
a b : α
⊢ ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
refine @(Multiset.induction_on t ?_ fun a t IH => ?_) <;> intros s u h₁ h₂
case pos
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u

case neg
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u
case refine_2
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
⊢ s ≤ (a ::ₘ t) ∩ u
by_cases h : a ∈ u
no goals
case refine_1
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t : Multiset α
a b : α
s u : Multiset α
h₁ : s ≤ 0
h₂ : s ≤ u
⊢ s ≤ 0 ∩ u
simpa only [zero_inter, nonpos_iff_eq_zero] using h₁
case pos
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ erase s a ≤ t ∩ erase u a
case pos
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u
rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]
no goals
case pos
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ erase s a ≤ t ∩ erase u a
exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)
case neg
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ t ∩ u
case neg
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u
rw [cons_inter_of_neg _ h]
no goals
case neg
α : Type u_1
β : Type ?u.175213
γ : Type ?u.175216
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ t ∩ u
exact IH ((le_cons_of_not_mem <| mt (mem_of_le h₂) h).1 h₁) h₂