-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_ofLists (L R : List PGame) :
    -ofLists L R = ofLists (R.map fun x => -x) (L.map fun x => -x)

Proof state:
case right
L R : List PGame
⊢ HEq (fun x => -L[↑x.down]) fun j => -L[↑j.down]

Tactic:
apply hfunext

Result:
case right.hα
L R : List PGame
⊢ ULift.{u_1, 0} (Fin L.length) = ULift.{u_1, 0} (Fin (List.map (fun x => -x) L).length)

case right.h
L R : List PGame
⊢ ∀ (a : ULift.{u_1, 0} (Fin L.length)) (a' : ULift.{u_1, 0} (Fin (List.map (fun x => -x) L).length)),
    HEq a a' → HEq (-L[↑a.down]) (-L[↑a'.down])

Proof state:
L R : List PGame
a : ℕ
ha : a < L.length
b✝ : ℕ
hb : b✝ < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b✝, hb⟩ }
m : ℕ
b : ULift.{?u.107178, 0} (Fin m)
⊢ ↑b.down = ↑b.down

Tactic:
rfl

Result:
no goals

Proof state:
case right.h.up.mk.up.mk.e_a.e_i
L R : List PGame
a : ℕ
ha : a < L.length
b : ℕ
hb : b < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b, hb⟩ }
this :
  ∀ {m n : ℕ},
    m = n → ∀ {b : ULift.{?u.107178, 0} (Fin m)} {c : ULift.{?u.107178, 0} (Fin n)}, HEq b c → ↑b.down = ↑c.down
⊢ a = b

Tactic:
exact this (List.length_map _ _).symm h

Result:
no goals

Proof state:
case right.h.up.mk.up.mk
L R : List PGame
a : ℕ
ha : a < L.length
b : ℕ
hb : b < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b, hb⟩ }
this :
  ∀ {m n : ℕ},
    m = n → ∀ {b : ULift.{?u.107178, 0} (Fin m)} {c : ULift.{?u.107178, 0} (Fin n)}, HEq b c → ↑b.down = ↑c.down
⊢ HEq (-L[↑{ down := ⟨a, ha⟩ }.down]) (-L[↑{ down := ⟨b, hb⟩ }.down])

Tactic:
simp only [heq_eq_eq]

Result:
case right.h.up.mk.up.mk
L R : List PGame
a : ℕ
ha : a < L.length
b : ℕ
hb : b < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b, hb⟩ }
this :
  ∀ {m n : ℕ},
    m = n → ∀ {b : ULift.{?u.107178, 0} (Fin m)} {c : ULift.{?u.107178, 0} (Fin n)}, HEq b c → ↑b.down = ↑c.down
⊢ -L[a] = -L[b]

Proof state:
L R : List PGame
a : ℕ
ha : a < L.length
b : ℕ
hb : b < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b, hb⟩ }
⊢ ∀ {m n : ℕ},
    m = n → ∀ {b : ULift.{?u.107178, 0} (Fin m)} {c : ULift.{?u.107178, 0} (Fin n)}, HEq b c → ↑b.down = ↑c.down

Tactic:
rintro m n rfl b c

Result:
L R : List PGame
a : ℕ
ha : a < L.length
b✝ : ℕ
hb : b✝ < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b✝, hb⟩ }
m : ℕ
b c : ULift.{?u.107178, 0} (Fin m)
⊢ HEq b c → ↑b.down = ↑c.down

Proof state:
L R : List PGame
⊢ -ofLists L R = ofLists (List.map (fun x => -x) R) (List.map (fun x => -x) L)

Tactic:
simp only [ofLists, neg_def, List.getElem_map, mk.injEq, List.length_map, true_and]

Result:
L R : List PGame
⊢ (HEq (fun x => -R[↑x.down]) fun i => -R[↑i.down]) ∧ HEq (fun x => -L[↑x.down]) fun j => -L[↑j.down]

Proof state:
L R : List PGame
a : ℕ
ha : a < L.length
b✝ : ℕ
hb : b✝ < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b✝, hb⟩ }
m : ℕ
b c : ULift.{?u.107178, 0} (Fin m)
⊢ HEq b c → ↑b.down = ↑c.down

Tactic:
simp only [heq_eq_eq]

Result:
L R : List PGame
a : ℕ
ha : a < L.length
b✝ : ℕ
hb : b✝ < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b✝, hb⟩ }
m : ℕ
b c : ULift.{?u.107178, 0} (Fin m)
⊢ b = c → ↑b.down = ↑c.down

Proof state:
case right.h
L R : List PGame
⊢ ∀ (a : ULift.{u_1, 0} (Fin L.length)) (a' : ULift.{u_1, 0} (Fin (List.map (fun x => -x) L).length)),
    HEq a a' → HEq (-L[↑a.down]) (-L[↑a'.down])

Tactic:
rintro ⟨⟨a, ha⟩⟩ ⟨⟨b, hb⟩⟩ h

Result:
case right.h.up.mk.up.mk
L R : List PGame
a : ℕ
ha : a < L.length
b : ℕ
hb : b < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b, hb⟩ }
⊢ HEq (-L[↑{ down := ⟨a, ha⟩ }.down]) (-L[↑{ down := ⟨b, hb⟩ }.down])

Proof state:
case right.h.up.mk.up.mk
L R : List PGame
a : ℕ
ha : a < L.length
b : ℕ
hb : b < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b, hb⟩ }
this :
  ∀ {m n : ℕ},
    m = n → ∀ {b : ULift.{?u.107178, 0} (Fin m)} {c : ULift.{?u.107178, 0} (Fin n)}, HEq b c → ↑b.down = ↑c.down
⊢ -L[a] = -L[b]

Tactic:
congr 5

Result:
case right.h.up.mk.up.mk.e_a.e_i
L R : List PGame
a : ℕ
ha : a < L.length
b : ℕ
hb : b < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b, hb⟩ }
this :
  ∀ {m n : ℕ},
    m = n → ∀ {b : ULift.{?u.107178, 0} (Fin m)} {c : ULift.{?u.107178, 0} (Fin n)}, HEq b c → ↑b.down = ↑c.down
⊢ a = b

Proof state:
L R : List PGame
a : ℕ
ha : a < L.length
b✝ : ℕ
hb : b✝ < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b✝, hb⟩ }
m : ℕ
b c : ULift.{?u.107178, 0} (Fin m)
⊢ b = c → ↑b.down = ↑c.down

Tactic:
rintro rfl

Result:
L R : List PGame
a : ℕ
ha : a < L.length
b✝ : ℕ
hb : b✝ < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b✝, hb⟩ }
m : ℕ
b : ULift.{?u.107178, 0} (Fin m)
⊢ ↑b.down = ↑b.down

Proof state:
case right.h.up.mk.up.mk
L R : List PGame
a : ℕ
ha : a < L.length
b : ℕ
hb : b < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b, hb⟩ }
⊢ HEq (-L[↑{ down := ⟨a, ha⟩ }.down]) (-L[↑{ down := ⟨b, hb⟩ }.down])

Tactic:
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

Result:
case right.h.up.mk.up.mk
L R : List PGame
a : ℕ
ha : a < L.length
b : ℕ
hb : b < (List.map (fun x => -x) L).length
h : HEq { down := ⟨a, ha⟩ } { down := ⟨b, hb⟩ }
this :
  ∀ {m n : ℕ},
    m = n → ∀ {b : ULift.{?u.107178, 0} (Fin m)} {c : ULift.{?u.107178, 0} (Fin n)}, HEq b c → ↑b.down = ↑c.down
⊢ HEq (-L[↑{ down := ⟨a, ha⟩ }.down]) (-L[↑{ down := ⟨b, hb⟩ }.down])

Proof state:
case right.hα
L R : List PGame
⊢ ULift.{u_1, 0} (Fin L.length) = ULift.{u_1, 0} (Fin (List.map (fun x => -x) L).length)

Tactic:
simp

Result:
no goals

Proof state:
L R : List PGame
⊢ (HEq (fun x => -R[↑x.down]) fun i => -R[↑i.down]) ∧ HEq (fun x => -L[↑x.down]) fun j => -L[↑j.down]

Tactic:
constructor

Result:
case left
L R : List PGame
⊢ HEq (fun x => -R[↑x.down]) fun i => -R[↑i.down]

case right
L R : List PGame
⊢ HEq (fun x => -L[↑x.down]) fun j => -L[↑j.down]