This PR changes the notion of minimality from being a set with an unbundled relation `r` (i.e. having type signature `minimals (r : α → α → Prop) (s : Set α) : Set α`) to being a predicate with a bundled order relation in a typeclass:  `Minimal [LE α] (P : α → Prop) : α → Prop`.
It also does the same for maximality. 

This is hopefully an improvement, for a few reasons : 
* ergonomic API with dot notation (eg `Minimal.eq_of_le`, `Minimal.not_lt`), 
* no need to specify a particular relation explicitly (no use of `minimals`/`maximals` for a relation that was not defeq to `LE.le` currently appears anywhere in mathlib),
* the potential in future to unify ad hoc notions of min/maximality appearing in various locations in mathlib (eg `zorn_preorder`, `Sylow.is_maximal'` to name a couple of random examples). 

Since this change removes the definitions `minimals` and `maximals` and all their API, it required a total overhaul of the contents of `Order.Minimal`, and necessarily required updating all uses of `maximals`/`minimals` elsewhere. There were not all too many of these; this PR is designed to be the smallest it could be while making this change. 

The changes required outside `Order.Minimal` were: 

- redefinition of `Ideal.minimalPrimes` in `RingTheory/Ideal/MinimalPrime` to use `Minimal` rather than `minimals`, with the necessary minor changes to proofs that used the old definition, including in `AlgebraicGeometry/PrimeSpectrum/Basic`.
- redefinition of `irreducibleComponents` in `Topology/Irreducible` to use `Minimal` rather than `minimals`, with necessary minor changes to proofs that used the old definition. 
- updating of the maximality used in the definition of a matroid in `Data/Matroid/Basic` from `maximals` to `Maximal`, with the necessary changes to everywhere in `Data/Matroid/*` that a matroid was specified using the definition directly. 
- the necessary changes to two lemmas in `Data/Finset/Lattice` that used `minimals`/`maximals` in the statements. 

I attempted to clean up the API in `Order.Minimal` to work smoothly with the new definitions, but numerous judgment calls were needed; I removed a few lemmas about `maximals/minimals` that were used nowhere, and seemed unlikely to be useful with the new definition.

Comment is welcome!

…5554)

We add a lemma stating that for `p : α -> Prop` we have `p = (· ∈ {a | p a})`. This lemma fills a gap that came up a couple of times when adapting `minimals` to the new `Minimal`, the alternative being an awkward `show`/`change` or `funext`. 

(See [this example from mathlib](#14721 (review)) (@j-loreaux 's first comment) and [this example](https://github.com/fpvandoorn/carleson/pull/109/files#r1705631209) from the Carleson project)

We change statements of Zorn's lemma to use the new `Maximal` API from #14721. The new definitions eliminate the need for separate `PartialOrder` and `Preorder` versions of Zorn's lemma, and slightly simplify most of its applications. 

The new statements of Zorn aren't defeq to the old ones, so a good number of files are touched, but very few theorem statements outside `Order.Zorn` itself are actually changed - most changes are small modifications of existing proofs. 

- [x] depends on: #14721

This PR changes the notion of minimality from being a set with an unbundled relation `r` (i.e. having type signature `minimals (r : α → α → Prop) (s : Set α) : Set α`) to being a predicate with a bundled order relation in a typeclass:  `Minimal [LE α] (P : α → Prop) : α → Prop`.
It also does the same for maximality. 

This is hopefully an improvement, for a few reasons : 
* ergonomic API with dot notation (eg `Minimal.eq_of_le`, `Minimal.not_lt`), 
* no need to specify a particular relation explicitly (no use of `minimals`/`maximals` for a relation that was not defeq to `LE.le` currently appears anywhere in mathlib),
* the potential in future to unify ad hoc notions of min/maximality appearing in various locations in mathlib (eg `zorn_preorder`, `Sylow.is_maximal'` to name a couple of random examples). 

Since this change removes the definitions `minimals` and `maximals` and all their API, it required a total overhaul of the contents of `Order.Minimal`, and necessarily required updating all uses of `maximals`/`minimals` elsewhere. There were not all too many of these; this PR is designed to be the smallest it could be while making this change. 

The changes required outside `Order.Minimal` were: 

- redefinition of `Ideal.minimalPrimes` in `RingTheory/Ideal/MinimalPrime` to use `Minimal` rather than `minimals`, with the necessary minor changes to proofs that used the old definition, including in `AlgebraicGeometry/PrimeSpectrum/Basic`.
- redefinition of `irreducibleComponents` in `Topology/Irreducible` to use `Minimal` rather than `minimals`, with necessary minor changes to proofs that used the old definition. 
- updating of the maximality used in the definition of a matroid in `Data/Matroid/Basic` from `maximals` to `Maximal`, with the necessary changes to everywhere in `Data/Matroid/*` that a matroid was specified using the definition directly. 
- the necessary changes to two lemmas in `Data/Finset/Lattice` that used `minimals`/`maximals` in the statements. 

I attempted to clean up the API in `Order.Minimal` to work smoothly with the new definitions, but numerous judgment calls were needed; I removed a few lemmas about `maximals/minimals` that were used nowhere, and seemed unlikely to be useful with the new definition.

Comment is welcome!

…5554)

We add a lemma stating that for `p : α -> Prop` we have `p = (· ∈ {a | p a})`. This lemma fills a gap that came up a couple of times when adapting `minimals` to the new `Minimal`, the alternative being an awkward `show`/`change` or `funext`. 

(See [this example from mathlib](#14721 (review)) (@j-loreaux 's first comment) and [this example](https://github.com/fpvandoorn/carleson/pull/109/files#r1705631209) from the Carleson project)

We change statements of Zorn's lemma to use the new `Maximal` API from #14721. The new definitions eliminate the need for separate `PartialOrder` and `Preorder` versions of Zorn's lemma, and slightly simplify most of its applications. 

The new statements of Zorn aren't defeq to the old ones, so a good number of files are touched, but very few theorem statements outside `Order.Zorn` itself are actually changed - most changes are small modifications of existing proofs. 

- [x] depends on: #14721

This PR changes the notion of minimality from being a set with an unbundled relation `r` (i.e. having type signature `minimals (r : α → α → Prop) (s : Set α) : Set α`) to being a predicate with a bundled order relation in a typeclass:  `Minimal [LE α] (P : α → Prop) : α → Prop`.
It also does the same for maximality. 

This is hopefully an improvement, for a few reasons : 
* ergonomic API with dot notation (eg `Minimal.eq_of_le`, `Minimal.not_lt`), 
* no need to specify a particular relation explicitly (no use of `minimals`/`maximals` for a relation that was not defeq to `LE.le` currently appears anywhere in mathlib),
* the potential in future to unify ad hoc notions of min/maximality appearing in various locations in mathlib (eg `zorn_preorder`, `Sylow.is_maximal'` to name a couple of random examples). 

Since this change removes the definitions `minimals` and `maximals` and all their API, it required a total overhaul of the contents of `Order.Minimal`, and necessarily required updating all uses of `maximals`/`minimals` elsewhere. There were not all too many of these; this PR is designed to be the smallest it could be while making this change. 

The changes required outside `Order.Minimal` were: 

- redefinition of `Ideal.minimalPrimes` in `RingTheory/Ideal/MinimalPrime` to use `Minimal` rather than `minimals`, with the necessary minor changes to proofs that used the old definition, including in `AlgebraicGeometry/PrimeSpectrum/Basic`.
- redefinition of `irreducibleComponents` in `Topology/Irreducible` to use `Minimal` rather than `minimals`, with necessary minor changes to proofs that used the old definition. 
- updating of the maximality used in the definition of a matroid in `Data/Matroid/Basic` from `maximals` to `Maximal`, with the necessary changes to everywhere in `Data/Matroid/*` that a matroid was specified using the definition directly. 
- the necessary changes to two lemmas in `Data/Finset/Lattice` that used `minimals`/`maximals` in the statements. 

I attempted to clean up the API in `Order.Minimal` to work smoothly with the new definitions, but numerous judgment calls were needed; I removed a few lemmas about `maximals/minimals` that were used nowhere, and seemed unlikely to be useful with the new definition.

Comment is welcome!

…5554)

We add a lemma stating that for `p : α -> Prop` we have `p = (· ∈ {a | p a})`. This lemma fills a gap that came up a couple of times when adapting `minimals` to the new `Minimal`, the alternative being an awkward `show`/`change` or `funext`. 

(See [this example from mathlib](#14721 (review)) (@j-loreaux 's first comment) and [this example](https://github.com/fpvandoorn/carleson/pull/109/files#r1705631209) from the Carleson project)

We change statements of Zorn's lemma to use the new `Maximal` API from #14721. The new definitions eliminate the need for separate `PartialOrder` and `Preorder` versions of Zorn's lemma, and slightly simplify most of its applications. 

The new statements of Zorn aren't defeq to the old ones, so a good number of files are touched, but very few theorem statements outside `Order.Zorn` itself are actually changed - most changes are small modifications of existing proofs. 

- [x] depends on: #14721

This PR changes the notion of minimality from being a set with an unbundled relation `r` (i.e. having type signature `minimals (r : α → α → Prop) (s : Set α) : Set α`) to being a predicate with a bundled order relation in a typeclass:  `Minimal [LE α] (P : α → Prop) : α → Prop`.
It also does the same for maximality. 

This is hopefully an improvement, for a few reasons : 
* ergonomic API with dot notation (eg `Minimal.eq_of_le`, `Minimal.not_lt`), 
* no need to specify a particular relation explicitly (no use of `minimals`/`maximals` for a relation that was not defeq to `LE.le` currently appears anywhere in mathlib),
* the potential in future to unify ad hoc notions of min/maximality appearing in various locations in mathlib (eg `zorn_preorder`, `Sylow.is_maximal'` to name a couple of random examples). 

Since this change removes the definitions `minimals` and `maximals` and all their API, it required a total overhaul of the contents of `Order.Minimal`, and necessarily required updating all uses of `maximals`/`minimals` elsewhere. There were not all too many of these; this PR is designed to be the smallest it could be while making this change. 

The changes required outside `Order.Minimal` were: 

- redefinition of `Ideal.minimalPrimes` in `RingTheory/Ideal/MinimalPrime` to use `Minimal` rather than `minimals`, with the necessary minor changes to proofs that used the old definition, including in `AlgebraicGeometry/PrimeSpectrum/Basic`.
- redefinition of `irreducibleComponents` in `Topology/Irreducible` to use `Minimal` rather than `minimals`, with necessary minor changes to proofs that used the old definition. 
- updating of the maximality used in the definition of a matroid in `Data/Matroid/Basic` from `maximals` to `Maximal`, with the necessary changes to everywhere in `Data/Matroid/*` that a matroid was specified using the definition directly. 
- the necessary changes to two lemmas in `Data/Finset/Lattice` that used `minimals`/`maximals` in the statements. 

I attempted to clean up the API in `Order.Minimal` to work smoothly with the new definitions, but numerous judgment calls were needed; I removed a few lemmas about `maximals/minimals` that were used nowhere, and seemed unlikely to be useful with the new definition.

Comment is welcome!

…5554)

We add a lemma stating that for `p : α -> Prop` we have `p = (· ∈ {a | p a})`. This lemma fills a gap that came up a couple of times when adapting `minimals` to the new `Minimal`, the alternative being an awkward `show`/`change` or `funext`. 

(See [this example from mathlib](#14721 (review)) (@j-loreaux 's first comment) and [this example](https://github.com/fpvandoorn/carleson/pull/109/files#r1705631209) from the Carleson project)

We change statements of Zorn's lemma to use the new `Maximal` API from #14721. The new definitions eliminate the need for separate `PartialOrder` and `Preorder` versions of Zorn's lemma, and slightly simplify most of its applications. 

The new statements of Zorn aren't defeq to the old ones, so a good number of files are touched, but very few theorem statements outside `Order.Zorn` itself are actually changed - most changes are small modifications of existing proofs. 

- [x] depends on: #14721