mathlib

5cb17dd1 - refactor(logic/is_empty): tag `is_empty.forall_iff` and `is_empty.exists_iff` as `simp` (#14660)

refactor(logic/is_empty): tag `is_empty.forall_iff` and `is_empty.exists_iff` as `simp` (#14660) We tag the lemmas `forall_iff` and `exists_iff` on empty types as `simp`. We remove `forall_pempty`, `exists_pempty`, `forall_false_left`, and `exists_false_left` due to being redundant.