feat: port apply_fun

[kim-em]

trafficstars

This will need minor additions once the tactic mono is ported, and some additional testing after Logic.Equiv.Basic and Order.Hom.Basic are ported.

[PatrickMassot]

Did you check that mathlib actually uses the part of apply_fun that uses mono? I think I wrote this because it seemed like a nice idea but I would be surprised to learn it is used a lot.

[kim-em]

Did you check that mathlib actually uses the part of apply_fun that uses mono? I think I wrote this because it seemed like a nice idea but I would be surprised to learn it is used a lot.

Yes, the build fails without it, perhaps just at category_theory/subobject/basic.lean line 533.

[digama0]

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style