mathlib

3cf2547c - feat(data/fintype/basic): Existence of a bijection with specified behaviour on a subset (#16479)

feat(data/fintype/basic): Existence of a bijection with specified behaviour on a subset (#16479) Given a function `f : α → β` which is injective on a set `s` in `α`, and a set `t` in `β` which has the same finite cardinality as the type `α` and which contains the image `f '' s`, extend/modify to a bijection between `α` and `t` which agrees on `s` with the original `f`.