α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Multiset α
⊢ filter p (s - t) = filter p s - filter p t
revert s
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (s - a ::ₘ t) = filter p s - filter p (a ::ₘ t)
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
refine' Multiset.induction_on t (by simp) fun a t IH s => _
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (erase s a) - filter p t = filter p s - filter p (a ::ₘ t)
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (s - a ::ₘ t) = filter p s - filter p (a ::ₘ t)
rw [sub_cons, IH]
case pos
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (erase s a) - filter p t = filter p s - filter p (a ::ₘ t)

case neg
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
⊢ filter p (erase s a) - filter p t = filter p s - filter p (a ::ₘ t)
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (erase s a) - filter p t = filter p s - filter p (a ::ₘ t)
by_cases h : p a
no goals
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - 0) = filter p s - filter p 0
simp
case pos
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (erase s a) - filter p t = erase (filter p s) a - filter p t
case pos
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (erase s a) - filter p t = filter p s - filter p (a ::ₘ t)
rw [filter_cons_of_pos _ h, sub_cons]
case pos.e_a
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (erase s a) = erase (filter p s) a
case pos
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (erase s a) - filter p t = erase (filter p s) a - filter p t
congr
case pos
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : a ∈ s
⊢ filter p (erase s a) = erase (filter p s) a

case neg
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : ¬a ∈ s
⊢ filter p (erase s a) = erase (filter p s) a
case pos.e_a
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (erase s a) = erase (filter p s) a
by_cases m : a ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : a ∈ s
⊢ filter p (erase s a) = erase (filter p s) a
rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h),
  cons_erase m]
no goals
case neg
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : ¬a ∈ s
⊢ filter p (erase s a) = erase (filter p s) a
rw [erase_of_not_mem m, erase_of_not_mem (mt mem_of_mem_filter m)]
case neg
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
⊢ filter p (erase s a) - filter p t = filter p s - filter p t
case neg
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
⊢ filter p (erase s a) - filter p t = filter p s - filter p (a ::ₘ t)
rw [filter_cons_of_neg _ h]
case pos
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
⊢ filter p (erase s a) - filter p t = filter p s - filter p t

case neg
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
⊢ filter p (erase s a) - filter p t = filter p s - filter p t
case neg
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
⊢ filter p (erase s a) - filter p t = filter p s - filter p t
by_cases m : a ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
⊢ filter p (erase s a) - filter p t = filter p s - filter p t
rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)),
  cons_erase m]
no goals
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
⊢ filter p (erase s a) = filter p (a ::ₘ erase s a)
rw [filter_cons_of_neg _ h]
no goals
case neg
α : Type u_1
β : Type ?u.237039
γ : Type ?u.237042
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
⊢ filter p (erase s a) - filter p t = filter p s - filter p t
rw [erase_of_not_mem m]