α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s - t + t ∩ s = s
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s - t + s ∩ t = s
rw [inter_comm]
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s t✝ u : Multiset α
a b : α
t : Multiset α
⊢ ∀ (s : Multiset α), s - t + t ∩ s = s
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s - t + t ∩ s = s
revert s
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s✝ t✝¹ u : Multiset α
a✝ b : α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s t✝ u : Multiset α
a b : α
t : Multiset α
⊢ ∀ (s : Multiset α), s - t + t ∩ s = s
refine' Multiset.induction_on t (by simp) fun a t IH s => _
case pos
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s✝ t✝¹ u : Multiset α
a✝ b : α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

case neg
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s✝ t✝¹ u : Multiset α
a✝ b : α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s✝ t✝¹ u : Multiset α
a✝ b : α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
by_cases h : a ∈ s
no goals
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s t✝ u : Multiset α
a b : α
t : Multiset α
⊢ ∀ (s : Multiset α), s - 0 + 0 ∩ s = s
simp
no goals
case pos
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s✝ t✝¹ u : Multiset α
a✝ b : α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
no goals
case neg
α : Type u_1
β : Type ?u.193543
γ : Type ?u.193546
inst✝ : DecidableEq α
s✝ t✝¹ u : Multiset α
a✝ b : α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
rw [cons_inter_of_neg _ h, sub_cons, erase_of_not_mem h, IH]