mathlib

d34b3306 - feat(data/set/basic,order/filter/basic): add semiconj lemmas about images and maps (#14970)

feat(data/set/basic,order/filter/basic): add semiconj lemmas about images and maps (#14970) This adds `function.commute` and `function.semiconj` lemmas, and replaces all the uses of `_comm` lemmas with the `semiconj` version as it turns out that only this generality is needed.