Commit 2025-08-13 00:55 59e4fba0

refactor: rename Rel to SetRel, restore the old Rel (#27447) Many users are confused that Rel no longer means what it used to. Since the design is not obvious (and the implementation is explicitly part of the interface thanks to abbrev), let's give it a name that makes the choice obvious. This then restores the old definition of Rel, as an abbrev; it's conceivable that many users were just using this as a shorthand, and this stops them being broken by #25587. Such users will of course be broken if they used the old API. This way, users bumping from 4.21.0 to 4.22.0 and using Rel only as a shorthand will not be broken. [#mathlib4 > Changing `Rel` to `Set (α × β)`, to help uniform spaces @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Changing.20.60Rel.60.20to.20.60Set.20.28.CE.B1.20.C3.97.20.CE.B2.29.60.2C.20to.20help.20uniform.20spaces/near/528531852)