α : Type u_1
β : Type ?u.271148
γ : Type ?u.271151
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s + 0 = s

α : Type u_1
β : Type ?u.271148
γ : Type ?u.271151
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)

α : Type u_1
β : Type ?u.271148
γ : Type ?u.271151
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → p a ∨ ¬p a
α : Type u_1
β : Type ?u.271148
γ : Type ?u.271151
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ filter p s + filter (fun a => ¬p a) s = s
rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]
no goals
α : Type u_1
β : Type ?u.271148
γ : Type ?u.271151
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s + 0 = s
simp only [add_zero]
no goals
α : Type u_1
β : Type ?u.271148
γ : Type ?u.271151
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)
simp [Decidable.em, -Bool.not_eq_true, -not_and, not_and_or, or_comm]
no goals
α : Type u_1
β : Type ?u.271148
γ : Type ?u.271151
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → p a ∨ ¬p a
simp only [Bool.not_eq_true, decide_eq_true_eq, Bool.eq_false_or_eq_true,
  decide_True, implies_true, Decidable.em]