mathlib3

b2427d53 - feat(order/filter/ultrafilter): Restriction of ultrafilters along large embeddings (#5195)

feat(order/filter/ultrafilter): Restriction of ultrafilters along large embeddings (#5195) This PR adds the fact that the `comap` of an ultrafilter along a "large" embedding (meaning the image is large w.r.t. the ultrafilter) is again an ultrafilter. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>