mathlib3

2aea9961 - feat(data): define a `fun_like` class of bundled homs (function + proofs) (#10286)

feat(data): define a `fun_like` class of bundled homs (function + proofs) (#10286) This PR introduces a class `fun_like` for types of bundled homomorphisms, like `set_like` is for bundled subobjects. This should be useful by itself, but an important use I see for it is the per-morphism class refactor, see #9888. Also, `coe_fn_coe_base` now has an appropriately low priority, so it doesn't take precedence over `fun_like.has_coe_to_fun`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>