x y : PGame
⊢ ((∃ i, x = moveRight (-y) i) ∨ ∃ i, x = moveLeft (-y) i) ↔ (∃ i, -x = moveLeft y i) ∨ ∃ i, -x = moveRight y i
x y : PGame
⊢ IsOption x (-y) ↔ IsOption (-x) y
rw [IsOption_iff, IsOption_iff, or_comm]
case mk
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((∃ i, x = moveRight (-mk α✝ β✝ a✝¹ a✝) i) ∨ ∃ i, x = moveLeft (-mk α✝ β✝ a✝¹ a✝) i) ↔
    (∃ i, -x = moveLeft (mk α✝ β✝ a✝¹ a✝) i) ∨ ∃ i, -x = moveRight (mk α✝ β✝ a✝¹ a✝) i
x y : PGame
⊢ ((∃ i, x = moveRight (-y) i) ∨ ∃ i, x = moveLeft (-y) i) ↔ (∃ i, -x = moveLeft y i) ∨ ∃ i, -x = moveRight y i
cases y
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ∀ (a : LeftMoves (-mk α✝ β✝ a✝¹ a✝)), x = moveLeft (-mk α✝ β✝ a✝¹ a✝) a ↔ -x = moveRight (mk α✝ β✝ a✝¹ a✝) a
case mk.h₂
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (∃ i, x = moveLeft (-mk α✝ β✝ a✝¹ a✝) i) ↔ ∃ i, -x = moveRight (mk α✝ β✝ a✝¹ a✝) i
apply exists_congr
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : LeftMoves (-mk α✝ β✝ a✝² a✝¹)
⊢ x = moveLeft (-mk α✝ β✝ a✝² a✝¹) a✝ ↔ -x = moveRight (mk α✝ β✝ a✝² a✝¹) a✝
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ∀ (a : LeftMoves (-mk α✝ β✝ a✝¹ a✝)), x = moveLeft (-mk α✝ β✝ a✝¹ a✝) a ↔ -x = moveRight (mk α✝ β✝ a✝¹ a✝) a
intro
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : LeftMoves (-mk α✝ β✝ a✝² a✝¹)
⊢ x = moveLeft (-mk α✝ β✝ a✝² a✝¹) a✝ ↔ x = -moveRight (mk α✝ β✝ a✝² a✝¹) a✝
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : LeftMoves (-mk α✝ β✝ a✝² a✝¹)
⊢ x = moveLeft (-mk α✝ β✝ a✝² a✝¹) a✝ ↔ -x = moveRight (mk α✝ β✝ a✝² a✝¹) a✝
rw [neg_eq_iff_eq_neg]
no goals
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : LeftMoves (-mk α✝ β✝ a✝² a✝¹)
⊢ x = moveLeft (-mk α✝ β✝ a✝² a✝¹) a✝ ↔ x = -moveRight (mk α✝ β✝ a✝² a✝¹) a✝
rfl