English
A synonym for Short.mk that specifies the pgame in an implicit argument, using given left and right moves data.
Русский
Синонім Short.mk, который задаётся через явное указание pgame и данные по ходам слева и справа.
LaTeX
$$Short.mk' {x : \mathrm{PGame}} [Fintype x.LeftMoves] [Fintype x.RightMoves] (sL : \forall i : x.LeftMoves, \mathrm{Short}(x.moveLeft i)) (sR : \forall j : x.RightMoves, \mathrm{Short}(x.moveRight j)) : \mathrm{Short}(x)$$
Lean4
/-- A synonym for `Short.mk` that specifies the pgame in an implicit argument. -/
def mk' {x : PGame} [Fintype x.LeftMoves] [Fintype x.RightMoves] (sL : ∀ i : x.LeftMoves, Short (x.moveLeft i))
(sR : ∀ j : x.RightMoves, Short (x.moveRight j)) : Short x := by
-- Porting note: Old proof relied on `unfreezingI`, which doesn't exist in Lean 4.
convert Short.mk sL sR
cases x
dsimp
