L R : List PGame
⊢ (HEq (fun j => -List.nthLe R ↑j.down (_ : ↑j.down < List.length R)) fun i =>
      -List.nthLe R ↑i.down (_ : ↑i.down < List.length R)) ∧
    HEq (fun i => -List.nthLe L ↑i.down (_ : ↑i.down < List.length L)) fun j =>
      -List.nthLe L ↑j.down (_ : ↑j.down < List.length L)
L R : List PGame
⊢ -ofLists L R = ofLists (List.map (fun x => -x) R) (List.map (fun x => -x) L)
simp only [ofLists, neg_def, List.length_map, List.nthLe_map', eq_self_iff_true, true_and,
  mk.injEq]
case left
L R : List PGame
⊢ HEq (fun j => -List.nthLe R ↑j.down (_ : ↑j.down < List.length R)) fun i =>
    -List.nthLe R ↑i.down (_ : ↑i.down < List.length R)

case right
L R : List PGame
⊢ HEq (fun i => -List.nthLe L ↑i.down (_ : ↑i.down < List.length L)) fun j =>
    -List.nthLe L ↑j.down (_ : ↑j.down < List.length L)
L R : List PGame
⊢ (HEq (fun j => -List.nthLe R ↑j.down (_ : ↑j.down < List.length R)) fun i =>
      -List.nthLe R ↑i.down (_ : ↑i.down < List.length R)) ∧
    HEq (fun i => -List.nthLe L ↑i.down (_ : ↑i.down < List.length L)) fun j =>
      -List.nthLe L ↑j.down (_ : ↑j.down < List.length L)
constructor
case right.hα
L R : List PGame
⊢ ULift (Fin (List.length L)) = ULift (Fin (List.length (List.map (fun x => -x) L)))

case right.h
L R : List PGame
⊢ ∀ (a : ULift (Fin (List.length L))) (a' : ULift (Fin (List.length (List.map (fun x => -x) L)))),
    HEq a a' →
      HEq (-List.nthLe L ↑a.down (_ : ↑a.down < List.length L)) (-List.nthLe L ↑a'.down (_ : ↑a'.down < List.length L))
case right
L R : List PGame
⊢ HEq (fun i => -List.nthLe L ↑i.down (_ : ↑i.down < List.length L)) fun j =>
    -List.nthLe L ↑j.down (_ : ↑j.down < List.length L)
apply hfunext
no goals
case right.hα
L R : List PGame
⊢ ULift (Fin (List.length L)) = ULift (Fin (List.length (List.map (fun x => -x) L)))
simp
case right.h
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
⊢ HEq (-List.nthLe L ↑a.down (_ : ↑a.down < List.length L)) (-List.nthLe L ↑a'.down (_ : ↑a'.down < List.length L))
case right.h
L R : List PGame
⊢ ∀ (a : ULift (Fin (List.length L))) (a' : ULift (Fin (List.length (List.map (fun x => -x) L)))),
    HEq a a' →
      HEq (-List.nthLe L ↑a.down (_ : ↑a.down < List.length L)) (-List.nthLe L ↑a'.down (_ : ↑a'.down < List.length L))
intro a a' ha
case right.h.h.e_a.e_n
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
⊢ ↑a.down = ↑a'.down
case right.h
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
⊢ HEq (-List.nthLe L ↑a.down (_ : ↑a.down < List.length L)) (-List.nthLe L ↑a'.down (_ : ↑a'.down < List.length L))
congr 2
case right.h.h.e_a.e_n
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
this : ∀ {m n : ℕ}, m = n → ∀ {b : ULift (Fin m)} {c : ULift (Fin n)}, HEq b c → ↑b.down = ↑c.down
⊢ ↑a.down = ↑a'.down
case right.h.h.e_a.e_n
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
⊢ ↑a.down = ↑a'.down
have :
  ∀ {m n} (_ : m = n) {b : ULift (Fin m)} {c : ULift (Fin n)} (_ : HEq b c),
    (b.down : ℕ) = ↑c.down := by
  rintro m n rfl b c
  simp only [heq_eq_eq]
  rintro rfl
  rfl
no goals
case right.h.h.e_a.e_n
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
this : ∀ {m n : ℕ}, m = n → ∀ {b : ULift (Fin m)} {c : ULift (Fin n)}, HEq b c → ↑b.down = ↑c.down
⊢ ↑a.down = ↑a'.down
exact this (List.length_map _ _).symm ha
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
m : ℕ
b c : ULift (Fin m)
⊢ HEq b c → ↑b.down = ↑c.down
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
⊢ ∀ {m n : ℕ}, m = n → ∀ {b : ULift (Fin m)} {c : ULift (Fin n)}, HEq b c → ↑b.down = ↑c.down
rintro m n rfl b c
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
m : ℕ
b c : ULift (Fin m)
⊢ b = c → ↑b.down = ↑c.down
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
m : ℕ
b c : ULift (Fin m)
⊢ HEq b c → ↑b.down = ↑c.down
simp only [heq_eq_eq]
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
m : ℕ
b : ULift (Fin m)
⊢ ↑b.down = ↑b.down
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
m : ℕ
b c : ULift (Fin m)
⊢ b = c → ↑b.down = ↑c.down
rintro rfl
no goals
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
m : ℕ
b : ULift (Fin m)
⊢ ↑b.down = ↑b.down
rfl