-- Mathlib/Data/Multiset/UnionInter.lean
lemma le_inter (h₁ : s ≤ t) (h₂ : s ≤ u) : s ≤ t ∩ u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u

Tactic:
refine @(Multiset.induction_on t ?_ fun a t IH => ?_) <;> intros s u h₁ h₂

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
t s u : Multiset α
h₁ : s ≤ 0
h₂ : s ≤ u
⊢ s ≤ 0 ∩ u

case refine_2
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
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

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
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

Tactic:
rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
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.erase a ≤ t ∩ u.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ t
h₂ : s ≤ u
⊢ s ≤ t ∩ u

Tactic:
revert s u

Result:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
t s u : Multiset α
h₁ : s ≤ 0
h₂ : s ≤ u
⊢ s ≤ 0 ∩ u

Tactic:
simpa only [zero_inter] using h₁

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
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

Tactic:
by_cases h : a ∈ u

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
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
inst✝ : DecidableEq α
t✝ : Multiset α
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

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
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

Tactic:
rw [cons_inter_of_neg _ h]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
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

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
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.erase a ≤ t ∩ u.erase a

Tactic:
exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
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

Tactic:
exact IH ((le_cons_of_not_mem <| mt (mem_of_le h₂) h).1 h₁) h₂

Result:
no goals