feat(order/lattice): Congruence lemmas for `⊔` and `⊓` (#15439)
`a ⊔ b = a ⊔ c` if `b ≤ a ⊔ c` and `c ≤ a ⊔ b`, and similar.
## Lemma renames
* `sup_eq_sup_of_le_le` → `sup_congr_right`
* `inf_eq_inf_of_le_le` → `inf_congr_right`
* `set.union_eq_union_of_subset_of_subset` → `set.union_congr_right`
* `set.inter_eq_inter_of_subset_of_subset` → `set.inter_congr_right`
