feat(nat, lattice): preliminaries for Haar measure (#3190)
PR 2/5 to put the Haar measure in mathlib. This PR: results about lattices and lattice operations on `nat`.
add some simp lemmas for `nat.find` (simplifying a proof in `sum_four_squares`)
rename `finset.sup_val` to `finset.sup_def` (it was unused). In PR 3 I will add a new declaration `finset.sup_val`
`Inf_nat_def` and `Sup_nat_def` renamed to `nat.Inf_def` and `nat.Sup_def`, and use `set.nonempty` in statement (they were unused outside that file)
