Set notation simp lemmas

Stream: mathlib4

[Alex Meiburg]

These two felt like "obvious" simp lemmas to me that I was surprised are not in mathlib:

@[simp]
theorem setOf_eq_empty_iff {α : Type*} (p : α → Prop) : { x | p x } = ∅ ↔ ∀ x, ¬p x :=
  Set.eq_empty_iff_forall_not_mem

@[simp]
theorem Finset.filter_univ_eq_empty_iff {α : Type*} [Fintype α] (p : α → Prop) [DecidablePred p] :
    ({ x | p x } : Finset α) = ∅ ↔ ∀ x, ¬p x :=
  ⟨by simp [Finset.filter_eq_empty_iff], (by simp [·])⟩

Neither one is proved by simp at the moment. I wanted to check if there was a reason they weren't - is this not a safe, confluent thing to rewrite with the global simp set, maybe? Or has it just not come up? (In that case I'll PR)

[Yury G. Kudryashov]

IMHO, docs#Finset.filter_eq_self and docs#Finset.filter_eq_empty_iff should be simp