Lean4
/-- Auxiliary construction of decidability instances.
We build `Decidable (x ≤ y)` and `Decidable (x ⧏ y)` in a simultaneous induction.
Instances for the two projections separately are provided below.
-/
def leLFDecidable : ∀ (x y : PGame.{u}) [Short x] [Short y], Decidable (x ≤ y) × Decidable (x ⧏ y)
| mk xl xr xL xR, mk yl yr yL yR, shortx, shorty => by
constructor
· refine @decidable_of_iff' _ _ mk_le_mk (id ?_)
have : Decidable (∀ (i : xl), xL i ⧏ mk yl yr yL yR) :=
by
apply @Fintype.decidableForallFintype xl _ ?_ _
intro i
apply (leLFDecidable _ _).2
have : Decidable (∀ (j : yr), mk xl xr xL xR ⧏ yR j) :=
by
apply @Fintype.decidableForallFintype yr _ ?_ _
intro i
apply (leLFDecidable _ _).2
exact inferInstanceAs (Decidable (_ ∧ _))
· refine @decidable_of_iff' _ _ mk_lf_mk (id ?_)
have : Decidable (∃ i, mk xl xr xL xR ≤ yL i) :=
by
apply @Fintype.decidableExistsFintype yl _ ?_ _
intro i
apply (leLFDecidable _ _).1
have : Decidable (∃ j, xR j ≤ mk yl yr yL yR) :=
by
apply @Fintype.decidableExistsFintype xr _ ?_ _
intro i
apply (leLFDecidable _ _).1
exact inferInstanceAs (Decidable (_ ∨ _))
termination_by x y => (x, y)
