fix(*): make some non-instances reducible (#7835)
* Definitions that involve in instances might need to be reducible, see added library note.
* This involves the definitions `*order.lift` / `function.injective.*` and `function.surjective.*`
* This came up in #7645.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
