feat(apply_fun): handle implicit arguments (#6091)
I've modified the way `apply_fun` handles inequalities, by building an intermediate expression before calling `mono` to discharge the `monotone f` subgoal. This has the effect of sometimes filling in implicit arguments successfully, so that `mono` works.
In `tests/apply_fun.lean` I've added an example showing this in action
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
