There is tension throughout the library between considering relations between `α` and `β` simply as `α → β → Prop`, or as a bundled object `Rel α β` with dedicated operations and API.

The former approach is used almost everywhere as it is very lightweight and has arguably native support from core Lean features, but it cracks at the seams whenever one starts talking about operations on relations. For example:
* composition of relations `R : α → β → Prop`, `S : β → γ → Prop` is the unwieldy `Relation.Comp R S := fun a c ↦ ∃ b, R a b ∧ S b c`
* map of a relation `R : α → β → Prop`, under `f : α → γ`, `g : β → δ` is the monstruous `Relation.map R f g := fun c d ↦ ∃ a b, r a b ∧ f a = c ∧ g b = d`.

The latter approach is embodied by the existing type `Rel α β`, with dedicated notation like `○` for composition. It makes it much easier to reason about operations relations, but currently its API suffers from the leakage of its definition as
```
def Rel (α β : Type*) := α → β → Prop
```
The fact that `Rel` isn't an `abbrev` confuses automation. But simply making it an `abbrev` would kill the point of having a separate less see-through type to perform relation operations on.

A final point, and the original motivation for this refactor, is that uniform spaces need a theory of relations on a type `α` as elements of  `Set (α × α)`. This cannot be worked around, since `Set (α × α)` is the type of elements of a filter on `α × α`. This theory is already developed in `Topology.UniformSpace.Defs`, and duplicates the existing `Rel` material.

This PR is a proposal to refactor `Rel` to be less see-through by redefining it as
```
abbrev Rel (α β : Type*) := Set (α × β)
```

This has several advantages:
* The use of `α × β` means that one can't abuse the defeq of `Rel α β` with the function type `α → β → Prop`.
* Instead, we get to provide an explicit notation `a ~[R] b` that very closely follows the paper convention `a ~R b` of using relations as infixes. This notation is scoped to the `Rel` namespace.
* The use of `Set` is an extra layer of indirection to avoid automation confusing `Rel α β` with `α × β → Prop`.
* It can directly be used in the theory of uniform spaces because of the syntactic equality between `Rel α α` and `Set (α × α)`.
* A relation can still be defined from an explicit function `α → β → Prop`, with nice notation: What was previously `fun a b ↦ R a b` becomes `{(a, b) | R a b}`.
* In general, fallout is manageably small and easily fixed by inserting the `{(a, b) | R a b}` and `a ~[R] b` notations.

The benefits can be seen in places like `CategoryTheory.Category.RelCat` where automation is significantly improved, or `Combinatorics.Hall.Basic` where defeq abuse is avoided and dot notation becomes available.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Uniform.20spaces.20and.20relations.20as.20sets)

There is tension throughout the library between considering relations between `α` and `β` simply as `α → β → Prop`, or as a bundled object `Rel α β` with dedicated operations and API.

The former approach is used almost everywhere as it is very lightweight and has arguably native support from core Lean features, but it cracks at the seams whenever one starts talking about operations on relations. For example:
* composition of relations `R : α → β → Prop`, `S : β → γ → Prop` is the unwieldy `Relation.Comp R S := fun a c ↦ ∃ b, R a b ∧ S b c`
* map of a relation `R : α → β → Prop`, under `f : α → γ`, `g : β → δ` is the monstruous `Relation.map R f g := fun c d ↦ ∃ a b, r a b ∧ f a = c ∧ g b = d`.

The latter approach is embodied by the existing type `Rel α β`, with dedicated notation like `○` for composition. It makes it much easier to reason about operations relations, but currently its API suffers from the leakage of its definition as
```
def Rel (α β : Type*) := α → β → Prop
```
The fact that `Rel` isn't an `abbrev` confuses automation. But simply making it an `abbrev` would kill the point of having a separate less see-through type to perform relation operations on.

A final point, and the original motivation for this refactor, is that uniform spaces need a theory of relations on a type `α` as elements of  `Set (α × α)`. This cannot be worked around, since `Set (α × α)` is the type of elements of a filter on `α × α`. This theory is already developed in `Topology.UniformSpace.Defs`, and duplicates the existing `Rel` material.

This PR is a proposal to refactor `Rel` to be less see-through by redefining it as
```
abbrev Rel (α β : Type*) := Set (α × β)
```

This has several advantages:
* The use of `α × β` means that one can't abuse the defeq of `Rel α β` with the function type `α → β → Prop`.
* Instead, we get to provide an explicit notation `a ~[R] b` that very closely follows the paper convention `a ~R b` of using relations as infixes. This notation is scoped to the `Rel` namespace.
* The use of `Set` is an extra layer of indirection to avoid automation confusing `Rel α β` with `α × β → Prop`.
* It can directly be used in the theory of uniform spaces because of the syntactic equality between `Rel α α` and `Set (α × α)`.
* A relation can still be defined from an explicit function `α → β → Prop`, with nice notation: What was previously `fun a b ↦ R a b` becomes `{(a, b) | R a b}`.
* In general, fallout is manageably small and easily fixed by inserting the `{(a, b) | R a b}` and `a ~[R] b` notations.

The benefits can be seen in places like `CategoryTheory.Category.RelCat` where automation is significantly improved, or `Combinatorics.Hall.Basic` where defeq abuse is avoided and dot notation becomes available.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Uniform.20spaces.20and.20relations.20as.20sets)

There is tension throughout the library between considering relations between `α` and `β` simply as `α → β → Prop`, or as a bundled object `Rel α β` with dedicated operations and API.

The former approach is used almost everywhere as it is very lightweight and has arguably native support from core Lean features, but it cracks at the seams whenever one starts talking about operations on relations. For example:
* composition of relations `R : α → β → Prop`, `S : β → γ → Prop` is the unwieldy `Relation.Comp R S := fun a c ↦ ∃ b, R a b ∧ S b c`
* map of a relation `R : α → β → Prop`, under `f : α → γ`, `g : β → δ` is the monstruous `Relation.map R f g := fun c d ↦ ∃ a b, r a b ∧ f a = c ∧ g b = d`.

The latter approach is embodied by the existing type `Rel α β`, with dedicated notation like `○` for composition. It makes it much easier to reason about operations relations, but currently its API suffers from the leakage of its definition as
```
def Rel (α β : Type*) := α → β → Prop
```
The fact that `Rel` isn't an `abbrev` confuses automation. But simply making it an `abbrev` would kill the point of having a separate less see-through type to perform relation operations on.

A final point, and the original motivation for this refactor, is that uniform spaces need a theory of relations on a type `α` as elements of  `Set (α × α)`. This cannot be worked around, since `Set (α × α)` is the type of elements of a filter on `α × α`. This theory is already developed in `Topology.UniformSpace.Defs`, and duplicates the existing `Rel` material.

This PR is a proposal to refactor `Rel` to be less see-through by redefining it as
```
abbrev Rel (α β : Type*) := Set (α × β)
```

This has several advantages:
* The use of `α × β` means that one can't abuse the defeq of `Rel α β` with the function type `α → β → Prop`.
* Instead, we get to provide an explicit notation `a ~[R] b` that very closely follows the paper convention `a ~R b` of using relations as infixes. This notation is scoped to the `Rel` namespace.
* The use of `Set` is an extra layer of indirection to avoid automation confusing `Rel α β` with `α × β → Prop`.
* It can directly be used in the theory of uniform spaces because of the syntactic equality between `Rel α α` and `Set (α × α)`.
* A relation can still be defined from an explicit function `α → β → Prop`, with nice notation: What was previously `fun a b ↦ R a b` becomes `{(a, b) | R a b}`.
* In general, fallout is manageably small and easily fixed by inserting the `{(a, b) | R a b}` and `a ~[R] b` notations.

The benefits can be seen in places like `CategoryTheory.Category.RelCat` where automation is significantly improved, or `Combinatorics.Hall.Basic` where defeq abuse is avoided and dot notation becomes available.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Uniform.20spaces.20and.20relations.20as.20sets)

There is tension throughout the library between considering relations between `α` and `β` simply as `α → β → Prop`, or as a bundled object `Rel α β` with dedicated operations and API.

The former approach is used almost everywhere as it is very lightweight and has arguably native support from core Lean features, but it cracks at the seams whenever one starts talking about operations on relations. For example:
* composition of relations `R : α → β → Prop`, `S : β → γ → Prop` is the unwieldy `Relation.Comp R S := fun a c ↦ ∃ b, R a b ∧ S b c`
* map of a relation `R : α → β → Prop`, under `f : α → γ`, `g : β → δ` is the monstruous `Relation.map R f g := fun c d ↦ ∃ a b, r a b ∧ f a = c ∧ g b = d`.

The latter approach is embodied by the existing type `Rel α β`, with dedicated notation like `○` for composition. It makes it much easier to reason about operations relations, but currently its API suffers from the leakage of its definition as
```
def Rel (α β : Type*) := α → β → Prop
```
The fact that `Rel` isn't an `abbrev` confuses automation. But simply making it an `abbrev` would kill the point of having a separate less see-through type to perform relation operations on.

A final point, and the original motivation for this refactor, is that uniform spaces need a theory of relations on a type `α` as elements of  `Set (α × α)`. This cannot be worked around, since `Set (α × α)` is the type of elements of a filter on `α × α`. This theory is already developed in `Topology.UniformSpace.Defs`, and duplicates the existing `Rel` material.

This PR is a proposal to refactor `Rel` to be less see-through by redefining it as
```
abbrev Rel (α β : Type*) := Set (α × β)
```

This has several advantages:
* The use of `α × β` means that one can't abuse the defeq of `Rel α β` with the function type `α → β → Prop`.
* Instead, we get to provide an explicit notation `a ~[R] b` that very closely follows the paper convention `a ~R b` of using relations as infixes. This notation is scoped to the `Rel` namespace.
* The use of `Set` is an extra layer of indirection to avoid automation confusing `Rel α β` with `α × β → Prop`.
* It can directly be used in the theory of uniform spaces because of the syntactic equality between `Rel α α` and `Set (α × α)`.
* A relation can still be defined from an explicit function `α → β → Prop`, with nice notation: What was previously `fun a b ↦ R a b` becomes `{(a, b) | R a b}`.
* In general, fallout is manageably small and easily fixed by inserting the `{(a, b) | R a b}` and `a ~[R] b` notations.

The benefits can be seen in places like `CategoryTheory.Category.RelCat` where automation is significantly improved, or `Combinatorics.Hall.Basic` where defeq abuse is avoided and dot notation becomes available.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Uniform.20spaces.20and.20relations.20as.20sets)

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](https://github.com/leanprover-community/mathlib4/blob/59bd63c72671849996d64c5d3b5f24a36333483c%5E/Mathlib/Data/Rel.lean).

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)

…-community#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 leanprover-community#25587. Such users will of course be broken if they used [the old API](https://github.com/leanprover-community/mathlib4/blob/59bd63c72671849996d64c5d3b5f24a36333483c%5E/Mathlib/Data/Rel.lean).

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 &leanprover-community#96;Rel&leanprover-community#96; to &leanprover-community#96;Set (α × β)&leanprover-community#96;, 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)

It used to be identical to its neighbor, `preimage_eq_dom_of_cod_subset`.
Both lemmas seem to have been introduced in #25587.

Co-authored-by: Pavel Grigorenko <GrigorenkoPV@ya.ru>

…rover-community#35696)

It used to be identical to its neighbor, `preimage_eq_dom_of_cod_subset`.
Both lemmas seem to have been introduced in leanprover-community#25587.

Co-authored-by: Pavel Grigorenko <GrigorenkoPV@ya.ru>