chore(SetTheory/Game/PGame): Equiv → AntisymmRel

[vihdzp]

We replace PGame.Equiv by the more general AntisymmRel. This is part of #19588.

We've kept both the setoid notation ≈, as well as equiv within theorem names. We've deprecated any results that are more generally true on preorders, save for those on LF which will be dealt with separately.

---

• depends on: [Merged by Bors] - feat(Order/Antisymmetrization): AntisymmRel lemmas #19571
• depends on: [Merged by Bors] - chore(SetTheory/Game/Impartial): golf two proofs #21074
• depends on: [Merged by Bors] - chore: add simp to Setoid.refl #21107

Although we can now define Game = Antisymmetrization PGame (· ≤ ·), doing so means that ⟦x⟧ notation breaks. Given that we can still use instPartialOrderAntisymmetrization to declare the partial order instance, it might not even be worth to do this redefinition. In any case, that probably should be discussed separately.

[github-actions]

PR summary 9a4093deaa

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.SetTheory.Game.PGame	483	484	+1 (+0.21%)
Mathlib.SetTheory.Game.Basic	534	535	+1 (+0.19%)
Mathlib.SetTheory.Game.Impartial	535	536	+1 (+0.19%)

Import changes for all files

Files	Import difference
3 files Mathlib.SetTheory.Game.Basic Mathlib.SetTheory.Game.Impartial Mathlib.SetTheory.Game.PGame	1

---

Declarations diff

+ equiv_of_equiv
+ equiv_of_exists
+ instance : @Trans PGame PGame PGame (· < ·) (· ≈ ·) (· < ·)
+ instance : @Trans PGame PGame PGame (· ≈ ·) (· < ·) (· < ·)
+ instance : @Trans PGame PGame PGame (· ≈ ·) (· ≤ ·) (· ≤ ·)
+ instance : @Trans PGame PGame PGame (· ≤ ·) (· ≈ ·) (· ≤ ·)
- instance : IsEquiv _ PGame.Equiv
---- instance : Trans

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.

---

Decrease in tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type
3841	-2	porting notes

Current commit 9a4093deaa
Reference commit b77fbf3757

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).

[LeoDog896]

I conceptually have no problem with this: redefining Equiv in this way is better towards the goal of better Game generalizations. I don't have any extra comments because I can't spot anything wrong with any of the formalization refactors, but I'm not experienced in that regard.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Order/Antisymmetrization): AntisymmRel lemmas #19571
• [Merged by Bors] - chore(SetTheory/Game/Impartial): golf two proofs #21074
• [Merged by Bors] - chore: add simp to Setoid.refl #21107
  By Dependent Issues (🤖). Happy coding!