refactor(data/set/basic): simpler proofs (#5920)
This replaces many uses of `simp` and `finish` with direct term proofs
to speed up the overall compilation of the file.
This PR is WIP in the sense that not all of `set.basic` is converted,
but there are no dependencies between the changes so this can be merged
at any point.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
