mathlib3

3d954923 - chore(data/set/lattice): move basic lemmas to basic files (#17882)

chore(data/set/lattice): move basic lemmas to basic files (#17882) This PR moves some lemmas in `data.set.lattice` to `data.set.basic`, `data.set.image`, and `data.set.function`. They are basic enough and do not depend on the set lattice. This also helps #17880 to split `data.set.pairwise` and reduce the dependency of many files. mathlib4 PR: https://github.com/leanprover-community/mathlib4/pull/1109