feat: add Coe (α → Bool) (α → Prop) and Coe (α → α → Bool) (α → α → Prop)

[kim-em]

I'm not sure if these are a terrible idea. They would be very convenient if they are not problematic...

Let's test and benchmark first and see where we stand.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b486c6748b153bda628575635baa28aeeb38b8c5 --onto 53e6e99a29362bc8069330f2bf045a10c8f65912. (2024-08-19 01:22:58)
• 💥 Mathlib branch lean-pr-testing-5088 build failed against this PR. (2024-08-19 02:20:52) View Log
• 🟡 Mathlib branch lean-pr-testing-5088 build against this PR was cancelled. (2024-08-19 10:59:28) View Log
• ✅ Mathlib branch lean-pr-testing-5088 has successfully built against this PR. (2024-08-19 12:05:46) View Log

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5c53692.
There were significant changes against commit 53e6e99:

  Benchmark   Metric             Change
  ===============================================
+ stdlib      fix level params    -1.3% (-14.1 σ)

[kim-em]

This does seem to slow Mathlib down appreciably, unfortunately, so I'll find another way.