chore(set_theory/zfc): general cleanup (#15208)
This PR does the following:
- Make `pSet.mk_type_func` into a `simp` lemma, rename to `pSet.eta`.
- Give a simpler definition for `pSet.empty`.
- Enable dot notation on `resp.equiv` and separate the `symm` and `trans` theorems from the `setoid` instance.
- Protect lemmas to avoid trouble between the `equiv` and the `resp.equiv` lemmas.
- Tweak some spacing.
- Add many missing `simp` tags.
