feat: define Squash as a Quotient

[vihdzp]

This PR changes the definition of Squash to use Quotient by upstreaming true_equivalence (now equivalence_true) and trueSetoid (now Setoid.trivial). The new definition is def-eq to the old one, but ensures that Squash can be used whenever a Quotient argument is expected without having to explicitly provide the setoid.

Besides being useful functionality, this makes Mathlib's Trunc completely equivalent to Squash. Mathlib PR #18952 will deprecate the former in favor of the latter.

[leanprover-community-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 9dbe5e6f9ce6bc686541218f62ff6b8063dfc4dc --onto e9bd9807ef7a983365df9ac55d35040d0b2d5ef2. (2025-01-14 16:17:35)
• 💥 Mathlib branch lean-pr-testing-6642 build failed against this PR. (2025-01-15 15:18:26) View Log

[kim-em]

@vihdzp, you can add the (newly required) changelog-* labels by commenting with the label name that you want. In this case I've added changelog-library for you.

[kim-em]

Please rebase onto nightly-with-mathlib and makes sure Mathlib is happy.

[vihdzp]

@kim-em FYI, I don't have permission to add labels myself.

[vihdzp]

The breakage here is due to Setoid.trivial being inferred in place of trivial. Should the former become protected?

[collares]

@kim-em FYI, I don't have permission to add labels myself.

If you add a comment containing just a label name, a bot automatically adds the corresponding label for you.