feat(order/complete_lattice): tweak simp lemmas

[vihdzp]

This PR marks Sup_range, supr_of_empty', supr_of_empty and their inf counterparts as simp. Further, the redundant supr_false and infi_false are removed in favor of supr_of_empty and infi_of_empty.

Note that marking Sup_range as simp means that by simp [supr] will loop. This affects a few simp coercion lemmas, but once those are proven, this doesn't seem to cause trouble.

---

• depends on: [Merged by Bors] - feat(data/{finset, set}/basic): tweak nonempty_coe_sort and is_empty_coe_sort #14937

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(data/{finset, set}/basic): tweak nonempty_coe_sort and is_empty_coe_sort #14937
  By Dependent Issues (🤖). Happy coding!

[vihdzp]

Making Sup_range a simp lemma was a bad idea, actually. Will re-do this with only the supr_empty change.