[Merged by Bors] - feat(Order/Cover): characterise covering in Pi types

[b-mehta]

Characterise the covering relation in products of partial orders.
Generalise this characterisation to products of preorders.
Use the characterisation to significantly simplify the characterisation of atoms in products of partial orders.

---

[github-actions]

PR summary 1157d7379a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ _root_.WCovBy.eval
+ covBy_iff
+ covBy_iff_antisymmRel
+ covBy_iff_exists_left_eq
+ covBy_iff_exists_right_eq
+ exists_forall_antisymmRel_of_covBy
+ exists_forall_antisymmRel_of_wcovBy
+ exists_forall_eq_of_covBy
+ exists_forall_eq_of_wcovBy
+ wcovBy_iff
+ wcovBy_iff_antisymmRel
+ wcovBy_iff_exists_left_eq
+ wcovBy_iff_exists_right_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[urkud]

Optional:

Suggested change

	lemma exists_forall_antisymmRel_of_covBy (h : a ⋖ b) :
	lemma _root_.CovBy.exists_forall_antisymmRel (h : a ⋖ b) :

[b-mehta]

I agree dot-notation here would be nice, but this loses the Pi mention of the original; which I think needs to be present here, and I don't see how to fit it nicely in the new name. Putting exists_forall_antisymmRel in the CovBy namespace without mentioning pi feels confusing to me

[urkud]

Optional, not sure if it's better:

Suggested change

	lemma wcovBy_iff' [Nonempty ι] :
	lemma wcovBy_iff_antisymmRel [Nonempty ι] :

[urkud]

Can you get left versions from OrderDual? Or do you consider it to be defeq abuse?

[b-mehta]

I think it is defeq abuse, but more importantly it seems quite a bit more painful to do: there's juggling between the order dual on each of the component types and on the pi type, and commuting the toDual/ofDual with Function.update; overall I don't think it's worth it.

[urkud]

I left some optional naming suggestions (move more theorems to WCovBy/CovBy namespaces). I'm not sure if they're actually better than the names you chose, so feel free to reject them. Thanks!
bors d+

[mathlib-bors]

✌️ b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[b-mehta]

Thanks for the review! I kept one batch of renames.

[b-mehta]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build