feat(data/equiv/basic): add `equiv.set.compl` (#4630)
Given an equivalence between two sets `e₀ : s ≃ t`, the set of
`e : α ≃ β` that agree with `e₀` on `s` is equivalent to `sᶜ ≃ tᶜ`.
Also add a bunch of lemmas to `data/set/function`; some of them are
used in the definition of `equiv.set.compl`.
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
