xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (((∀ (i : yr), -yR i ⧏ -mk xl xr (fun i => xL i) fun j => xR j) ∧
        ∀ (j : xl), (-mk yl yr (fun i => yL i) fun j => yR j) ⧏ -xL j) ↔
      (∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j) ∧
    (((∃ i, (-mk yl yr (fun i => yL i) fun j => yR j) ≤ -xR i) ∨ ∃ j, -yL j ≤ -mk xl xr (fun i => xL i) fun j => xR j) ↔
      (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR)
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (-mk yl yr yL yR ≤ -mk xl xr xL xR ↔ mk xl xr xL xR ≤ mk yl yr yL yR) ∧
    (-mk yl yr yL yR ⧏ -mk xl xr xL xR ↔ mk xl xr xL xR ⧏ mk yl yr yL yR)
simp_rw [neg_def, mk_le_mk, mk_lf_mk, ← neg_def]
case left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∀ (i : yr), -yR i ⧏ -mk xl xr (fun i => xL i) fun j => xR j) ∧
      ∀ (j : xl), (-mk yl yr (fun i => yL i) fun j => yR j) ⧏ -xL j) ↔
    (∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j

case right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∃ i, (-mk yl yr (fun i => yL i) fun j => yR j) ≤ -xR i) ∨ ∃ j, -yL j ≤ -mk xl xr (fun i => xL i) fun j => xR j) ↔
    (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (((∀ (i : yr), -yR i ⧏ -mk xl xr (fun i => xL i) fun j => xR j) ∧
        ∀ (j : xl), (-mk yl yr (fun i => yL i) fun j => yR j) ⧏ -xL j) ↔
      (∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j) ∧
    (((∃ i, (-mk yl yr (fun i => yL i) fun j => yR j) ≤ -xR i) ∨ ∃ j, -yL j ≤ -mk xl xr (fun i => xL i) fun j => xR j) ↔
      (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR)
constructor
case left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∀ (j : xl), (-mk yl yr (fun i => yL i) fun j => yR j) ⧏ -xL j) ∧
      ∀ (i : yr), -yR i ⧏ -mk xl xr (fun i => xL i) fun j => xR j) ↔
    (∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j
case left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∀ (i : yr), -yR i ⧏ -mk xl xr (fun i => xL i) fun j => xR j) ∧
      ∀ (j : xl), (-mk yl yr (fun i => yL i) fun j => yR j) ⧏ -xL j) ↔
    (∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j
rw [and_comm]
no goals
case left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∀ (j : xl), (-mk yl yr (fun i => yL i) fun j => yR j) ⧏ -xL j) ∧
      ∀ (i : yr), -yR i ⧏ -mk xl xr (fun i => xL i) fun j => xR j) ↔
    (∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j
apply and_congr <;> exact forall_congr' fun _ => neg_le_lf_neg_iff.2
case right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∃ j, -yL j ≤ -mk xl xr (fun i => xL i) fun j => xR j) ∨ ∃ i, (-mk yl yr (fun i => yL i) fun j => yR j) ≤ -xR i) ↔
    (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR
case right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∃ i, (-mk yl yr (fun i => yL i) fun j => yR j) ≤ -xR i) ∨ ∃ j, -yL j ≤ -mk xl xr (fun i => xL i) fun j => xR j) ↔
    (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR
rw [or_comm]
no goals
case right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∃ j, -yL j ≤ -mk xl xr (fun i => xL i) fun j => xR j) ∨ ∃ i, (-mk yl yr (fun i => yL i) fun j => yR j) ≤ -xR i) ↔
    (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR
apply or_congr <;> exact exists_congr fun _ => neg_le_lf_neg_iff.1