[Merged by Bors] - feat: define PGame.identical PGame.memₗ PGame.memᵣ

[FR-vdash-bot]

---

split from #5901

[github-actions]

PR summary 70db6730f9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Identical
+ Identical.congr_left
+ Identical.congr_right
+ Identical.equiv
+ Identical.ext
+ Identical.ext_iff
+ Identical.ge
+ Identical.le
+ Identical.moveLeft
+ Identical.moveRight
+ Identical.of_equiv
+ Identical.of_fn
+ Identical.refl
+ Identical.rfl
+ Identical.symm
+ Identical.trans
+ identicalSetoid
+ identical_comm
+ identical_iff
+ identical_iff'
+ identical_of_isEmpty
+ instance : IsEquiv PGame (· ≡ ·) := { }
+ instance : IsRefl PGame (· ≡ ·) := ⟨Identical.refl⟩
+ instance : IsSymm PGame (· ≡ ·) := ⟨fun _ _ ↦ Identical.symm⟩
+ instance : IsTrans PGame (· ≡ ·) := ⟨fun _ _ _ ↦ Identical.trans⟩
+ memᵣ
+ memᵣ.congr_left
+ memᵣ.congr_right
+ memᵣ_def
+ memₗ
+ memₗ.congr_left
+ memₗ.congr_right
+ memₗ_def
+ moveLeft_memₗ
+ moveRight_memᵣ

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

[vihdzp]

Thanks for splitting this up! I was worried the original PR would stay in limbo due to how overarching it was.

[vihdzp]

This looks great! I'm excited to soon have the legendary IGame as a part of Mathlib.

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style