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>

Author: digama0