feat(tactic/apply_fun): work on the goal as well (#6439)
Extend the functionality of `apply_fun`, to "apply" functions to inequalities in the goal, as well.
```
Apply a function to an equality or inequality in either a local hypothesis or the goal.
* If we have `h : a = b`, then `apply_fun f at h` will replace this with `h : f a = f b`.
* If we have `h : a ≤ b`, then `apply_fun f at h` will replace this with `h : f a ≤ f b`,
and create a subsidiary goal `monotone f`.
`apply_fun` will automatically attempt to discharge this subsidiary goal using `mono`,
or an explicit solution can be provided with `apply_fun f at h using P`, where `P : monotone f`.
* If the goal is `a ≠ b`, `apply_fun f` will replace this with `f a ≠ f b`.
* If the goal is `a = b`, `apply_fun f` will replace this with `f a = f b`,
and create a subsidiary goal `injective f`.
`apply_fun` will automatically attempt to discharge this subsidiary goal using local hypotheses,
or if `f` is actually an `equiv`,
or an explicit solution can be provided with `apply_fun f using P`, where `P : injective f`.
* If the goal is `a ≤ b` (or similarly for `a < b`), and `f` is actually an `order_iso`,
`apply_fun f` will replace the goal with `f a ≤ f b`.
If `f` is anything else (e.g. just a function, or an `equiv`), `apply_fun` will fail.
```
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
