English
If there is a complete correspondence between the moves of x and y given by left/right mappings, then x ≡ y.
Русский
Если существует полное соответствие ходов x и y через соответствие левых и правых ходов, то x ≡ y.
LaTeX
$$$ \forall x,y,\ (l : x.LeftMoves \to y.LeftMoves) \ (il : y.LeftMoves \to x.LeftMoves) \ (r : x.RightMoves \to y.RightMoves) \ (ir : y.RightMoves \to x.RightMoves) \\ \\ (hl : \forall i, x.moveLeft i \equiv y.moveLeft (l i)) \ (hil : \forall i, x.moveLeft (il i) \equiv y.moveLeft i) \\ (hr : \forall i, x.moveRight i \equiv y.moveRight (r i)) \ (hir : \forall i, x.moveRight (ir i) \equiv y.moveRight i) : x \equiv y$$$
Lean4
/-- Show `x ≡ y` by giving an explicit correspondence between the moves of `x` and `y`. -/
theorem of_fn {x y : PGame} (l : x.LeftMoves → y.LeftMoves) (il : y.LeftMoves → x.LeftMoves)
(r : x.RightMoves → y.RightMoves) (ir : y.RightMoves → x.RightMoves) (hl : ∀ i, x.moveLeft i ≡ y.moveLeft (l i))
(hil : ∀ i, x.moveLeft (il i) ≡ y.moveLeft i) (hr : ∀ i, x.moveRight i ≡ y.moveRight (r i))
(hir : ∀ i, x.moveRight (ir i) ≡ y.moveRight i) : x ≡ y :=
identical_iff.mpr ⟨⟨fun i ↦ ⟨l i, hl i⟩, fun i ↦ ⟨il i, hil i⟩⟩, ⟨fun i ↦ ⟨r i, hr i⟩, fun i ↦ ⟨ir i, hir i⟩⟩⟩
