[GOAL]
a✝ : PGame
G : PGame := a✝
i : LeftMoves G
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (moveLeft G i) a✝
[PROOFSTEP]
pgame_wf_tac
[GOAL]
a✝ : PGame
G : PGame := a✝
j : RightMoves G
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (moveRight G j) a✝
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G : PGame
⊢ ImpartialAux G ↔
    G ≈ -G ∧ (∀ (i : LeftMoves G), ImpartialAux (moveLeft G i)) ∧ ∀ (j : RightMoves G), ImpartialAux (moveRight G j)
[PROOFSTEP]
rw [ImpartialAux]
[GOAL]
G : PGame
⊢ Impartial G ↔
    G ≈ -G ∧ (∀ (i : LeftMoves G), Impartial (moveLeft G i)) ∧ ∀ (j : RightMoves G), Impartial (moveRight G j)
[PROOFSTEP]
simpa only [impartial_iff_aux] using impartialAux_def
[GOAL]
⊢ Impartial 0
[PROOFSTEP]
rw [impartial_def]
[GOAL]
⊢ 0 ≈ -0 ∧ (∀ (i : LeftMoves 0), Impartial (moveLeft 0 i)) ∧ ∀ (j : RightMoves 0), Impartial (moveRight 0 j)
[PROOFSTEP]
dsimp
[GOAL]
⊢ 0 ≈ -0 ∧ (∀ (i : PEmpty), Impartial (moveLeft 0 i)) ∧ ∀ (j : PEmpty), Impartial (moveRight 0 j)
[PROOFSTEP]
simp
[GOAL]
⊢ Impartial star
[PROOFSTEP]
rw [impartial_def]
[GOAL]
⊢ star ≈ -star ∧
    (∀ (i : LeftMoves star), Impartial (moveLeft star i)) ∧ ∀ (j : RightMoves star), Impartial (moveRight star j)
[PROOFSTEP]
simpa using Impartial.impartial_zero
[GOAL]
G H : PGame
e : G ≡r H
⊢ ∀ [inst : Impartial G], Impartial H
[PROOFSTEP]
intro h
[GOAL]
G H : PGame
e : G ≡r H
h : Impartial G
⊢ Impartial H
[PROOFSTEP]
exact
  impartial_def.2
    ⟨Equiv.trans e.symm.equiv (Equiv.trans (neg_equiv_self G) (neg_equiv_neg_iff.2 e.equiv)), fun i =>
      impartial_congr (e.moveLeftSymm i), fun j => impartial_congr (e.moveRightSymm j)⟩
[GOAL]
G H : PGame
x✝ :
  ∀ (y : (_ : PGame) ×' PGame),
    (invImage (fun a => PSigma.casesOn a fun G snd => (G, snd)) Prod.instWellFoundedRelationProd).1 y
        { fst := G, snd := H } →
      y.1 ≡r y.2 → ∀ [inst : Impartial y.1], Impartial y.2
e : G ≡r H
h : Impartial G
i : LeftMoves H
⊢ (invImage (fun a => PSigma.casesOn a fun G snd => (G, snd)) Prod.instWellFoundedRelationProd).1
    { fst := moveLeft G (↑(Relabelling.leftMovesEquiv e).symm i), snd := moveLeft H i } { fst := G, snd := H }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G H : PGame
x✝ :
  ∀ (y : (_ : PGame) ×' PGame),
    (invImage (fun a => PSigma.casesOn a fun G snd => (G, snd)) Prod.instWellFoundedRelationProd).1 y
        { fst := G, snd := H } →
      y.1 ≡r y.2 → ∀ [inst : Impartial y.1], Impartial y.2
e : G ≡r H
h : Impartial G
j : RightMoves H
⊢ (invImage (fun a => PSigma.casesOn a fun G snd => (G, snd)) Prod.instWellFoundedRelationProd).1
    { fst := moveRight G (↑(Relabelling.rightMovesEquiv e).symm j), snd := moveRight H j } { fst := G, snd := H }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
⊢ Impartial (G + H)
[PROOFSTEP]
rw [impartial_def]
[GOAL]
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
⊢ G + H ≈ -(G + H) ∧
    (∀ (i : LeftMoves (G + H)), Impartial (moveLeft (G + H) i)) ∧
      ∀ (j : RightMoves (G + H)), Impartial (moveRight (G + H) j)
[PROOFSTEP]
refine'
  ⟨Equiv.trans (add_congr (neg_equiv_self G) (neg_equiv_self _)) (Equiv.symm (negAddRelabelling _ _).equiv), fun k => _,
    fun k => _⟩
[GOAL]
case refine'_1
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
⊢ Impartial (moveLeft (G + H) k)
[PROOFSTEP]
apply leftMoves_add_cases k
[GOAL]
case refine'_1.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
⊢ ∀ (i : LeftMoves G), Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inl i)))
case refine'_1.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
⊢ ∀ (i : LeftMoves H), Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inr i)))
[PROOFSTEP]
all_goals
  intro i; simp only [add_moveLeft_inl, add_moveLeft_inr]
  apply impartial_add
[GOAL]
case refine'_1.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
⊢ ∀ (i : LeftMoves G), Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inl i)))
[PROOFSTEP]
intro i
[GOAL]
case refine'_1.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
i : LeftMoves G
⊢ Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inl i)))
[PROOFSTEP]
simp only [add_moveLeft_inl, add_moveLeft_inr]
[GOAL]
case refine'_1.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
i : LeftMoves G
⊢ Impartial (moveLeft G i + H)
[PROOFSTEP]
apply impartial_add
[GOAL]
case refine'_1.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
⊢ ∀ (i : LeftMoves H), Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inr i)))
[PROOFSTEP]
intro i
[GOAL]
case refine'_1.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
i : LeftMoves H
⊢ Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inr i)))
[PROOFSTEP]
simp only [add_moveLeft_inl, add_moveLeft_inr]
[GOAL]
case refine'_1.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
i : LeftMoves H
⊢ Impartial (G + moveLeft H i)
[PROOFSTEP]
apply impartial_add
[GOAL]
case refine'_2
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
⊢ Impartial (moveRight (G + H) k)
[PROOFSTEP]
apply rightMoves_add_cases k
[GOAL]
case refine'_2.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
⊢ ∀ (j : RightMoves G), Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inl j)))
case refine'_2.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
⊢ ∀ (j : RightMoves H), Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inr j)))
[PROOFSTEP]
all_goals
  intro i; simp only [add_moveRight_inl, add_moveRight_inr]
  apply impartial_add
[GOAL]
case refine'_2.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
⊢ ∀ (j : RightMoves G), Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inl j)))
[PROOFSTEP]
intro i
[GOAL]
case refine'_2.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
i : RightMoves G
⊢ Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inl i)))
[PROOFSTEP]
simp only [add_moveRight_inl, add_moveRight_inr]
[GOAL]
case refine'_2.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
i : RightMoves G
⊢ Impartial (moveRight G i + H)
[PROOFSTEP]
apply impartial_add
[GOAL]
case refine'_2.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
⊢ ∀ (j : RightMoves H), Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inr j)))
[PROOFSTEP]
intro i
[GOAL]
case refine'_2.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
i : RightMoves H
⊢ Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inr i)))
[PROOFSTEP]
simp only [add_moveRight_inl, add_moveRight_inr]
[GOAL]
case refine'_2.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
i : RightMoves H
⊢ Impartial (G + moveRight H i)
[PROOFSTEP]
apply impartial_add
[GOAL]
G H : PGame
x✝² : Impartial G
x✝¹ : Impartial H
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Impartial x) ×' Impartial x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
            Prod.instWellFoundedRelationProd).1
        y { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } } →
      Impartial (y.1 + y.2.1)
i : LeftMoves G
⊢ (invImage
        (fun a => PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
        Prod.instWellFoundedRelationProd).1
    { fst := moveLeft G i, snd := { fst := H, snd := { fst := (_ : Impartial (moveLeft G i)), snd := x✝¹ } } }
    { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G H : PGame
x✝² : Impartial G
x✝¹ : Impartial H
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Impartial x) ×' Impartial x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
            Prod.instWellFoundedRelationProd).1
        y { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } } →
      Impartial (y.1 + y.2.1)
i : LeftMoves H
⊢ (invImage
        (fun a => PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
        Prod.instWellFoundedRelationProd).1
    { fst := G, snd := { fst := moveLeft H i, snd := { fst := x✝², snd := (_ : Impartial (moveLeft H i)) } } }
    { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G H : PGame
x✝² : Impartial G
x✝¹ : Impartial H
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Impartial x) ×' Impartial x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
            Prod.instWellFoundedRelationProd).1
        y { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } } →
      Impartial (y.1 + y.2.1)
i : RightMoves G
⊢ (invImage
        (fun a => PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
        Prod.instWellFoundedRelationProd).1
    { fst := moveRight G i, snd := { fst := H, snd := { fst := (_ : Impartial (moveRight G i)), snd := x✝¹ } } }
    { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G H : PGame
x✝² : Impartial G
x✝¹ : Impartial H
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Impartial x) ×' Impartial x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
            Prod.instWellFoundedRelationProd).1
        y { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } } →
      Impartial (y.1 + y.2.1)
i : RightMoves H
⊢ (invImage
        (fun a => PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
        Prod.instWellFoundedRelationProd).1
    { fst := G, snd := { fst := moveRight H i, snd := { fst := x✝², snd := (_ : Impartial (moveRight H i)) } } }
    { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G : PGame
x✝ : Impartial G
⊢ Impartial (-G)
[PROOFSTEP]
rw [impartial_def]
[GOAL]
G : PGame
x✝ : Impartial G
⊢ -G ≈ - -G ∧
    (∀ (i : LeftMoves (-G)), Impartial (moveLeft (-G) i)) ∧ ∀ (j : RightMoves (-G)), Impartial (moveRight (-G) j)
[PROOFSTEP]
refine' ⟨_, fun i => _, fun i => _⟩
[GOAL]
case refine'_1
G : PGame
x✝ : Impartial G
⊢ -G ≈ - -G
[PROOFSTEP]
rw [neg_neg]
[GOAL]
case refine'_1
G : PGame
x✝ : Impartial G
⊢ -G ≈ G
[PROOFSTEP]
exact Equiv.symm (neg_equiv_self G)
[GOAL]
case refine'_2
G : PGame
x✝ : Impartial G
i : LeftMoves (-G)
⊢ Impartial (moveLeft (-G) i)
[PROOFSTEP]
rw [moveLeft_neg']
[GOAL]
case refine'_2
G : PGame
x✝ : Impartial G
i : LeftMoves (-G)
⊢ Impartial (-moveRight G (↑toLeftMovesNeg.symm i))
[PROOFSTEP]
apply impartial_neg
[GOAL]
case refine'_3
G : PGame
x✝ : Impartial G
i : RightMoves (-G)
⊢ Impartial (moveRight (-G) i)
[PROOFSTEP]
rw [moveRight_neg']
[GOAL]
case refine'_3
G : PGame
x✝ : Impartial G
i : RightMoves (-G)
⊢ Impartial (-moveLeft G (↑toRightMovesNeg.symm i))
[PROOFSTEP]
apply impartial_neg
[GOAL]
G : PGame
x✝¹ : Impartial G
x✝ :
  ∀ (y : (x : PGame) ×' Impartial x),
    (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1 y { fst := G, snd := x✝¹ } →
      Impartial (-y.1)
i : LeftMoves (-G)
⊢ (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1
    { fst := moveRight G (↑toLeftMovesNeg.symm i), snd := (_ : Impartial (moveRight G (↑toLeftMovesNeg.symm i))) }
    { fst := G, snd := x✝¹ }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G : PGame
x✝¹ : Impartial G
x✝ :
  ∀ (y : (x : PGame) ×' Impartial x),
    (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1 y { fst := G, snd := x✝¹ } →
      Impartial (-y.1)
i : RightMoves (-G)
⊢ (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1
    { fst := moveLeft G (↑toRightMovesNeg.symm i), snd := (_ : Impartial (moveLeft G (↑toRightMovesNeg.symm i))) }
    { fst := G, snd := x✝¹ }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G : PGame
inst✝ : Impartial G
h : 0 < G
⊢ False
[PROOFSTEP]
have h' := neg_lt_neg_iff.2 h
[GOAL]
G : PGame
inst✝ : Impartial G
h : 0 < G
h' : -G < -0
⊢ False
[PROOFSTEP]
rw [neg_zero, lt_congr_left (Equiv.symm (neg_equiv_self G))] at h' 
[GOAL]
G : PGame
inst✝ : Impartial G
h : 0 < G
h' : G < 0
⊢ False
[PROOFSTEP]
exact (h.trans h').false
[GOAL]
G : PGame
inst✝ : Impartial G
h : G < 0
⊢ False
[PROOFSTEP]
have h' := neg_lt_neg_iff.2 h
[GOAL]
G : PGame
inst✝ : Impartial G
h : G < 0
h' : -0 < -G
⊢ False
[PROOFSTEP]
rw [neg_zero, lt_congr_right (Equiv.symm (neg_equiv_self G))] at h' 
[GOAL]
G : PGame
inst✝ : Impartial G
h : G < 0
h' : 0 < G
⊢ False
[PROOFSTEP]
exact (h.trans h').false
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ G ≈ 0 ∨ G ‖ 0
[PROOFSTEP]
rcases lt_or_equiv_or_gt_or_fuzzy G 0 with (h | h | h | h)
[GOAL]
case inl
G : PGame
inst✝ : Impartial G
h : G < 0
⊢ G ≈ 0 ∨ G ‖ 0
[PROOFSTEP]
exact ((nonneg G) h).elim
[GOAL]
case inr.inl
G : PGame
inst✝ : Impartial G
h : G ≈ 0
⊢ G ≈ 0 ∨ G ‖ 0
[PROOFSTEP]
exact Or.inl h
[GOAL]
case inr.inr.inl
G : PGame
inst✝ : Impartial G
h : 0 < G
⊢ G ≈ 0 ∨ G ‖ 0
[PROOFSTEP]
exact ((nonpos G) h).elim
[GOAL]
case inr.inr.inr
G : PGame
inst✝ : Impartial G
h : G ‖ 0
⊢ G ≈ 0 ∨ G ‖ 0
[PROOFSTEP]
exact Or.inr h
[GOAL]
G : PGame
inst✝ : Impartial G
H : PGame
⊢ H ≈ G ↔ H + G ≈ 0
[PROOFSTEP]
rw [Game.PGame.equiv_iff_game_eq, ← @add_right_cancel_iff _ _ _ ⟦G⟧, mk'_add_self, ← quot_add,
  Game.PGame.equiv_iff_game_eq]
[GOAL]
G : PGame
inst✝ : Impartial G
H : PGame
⊢ Quotient.mk setoid (H + G) = 0 ↔ Quotient.mk setoid (H + G) = Quotient.mk setoid 0
[PROOFSTEP]
rfl
[GOAL]
G : PGame
inst✝ : Impartial G
H : PGame
⊢ G ≈ H ↔ G + H ≈ 0
[PROOFSTEP]
rw [Game.PGame.equiv_iff_game_eq, ← @add_left_cancel_iff _ _ _ ⟦G⟧, mk'_add_self, ← quot_add,
  Game.PGame.equiv_iff_game_eq]
[GOAL]
G : PGame
inst✝ : Impartial G
H : PGame
⊢ 0 = Quotient.mk setoid (G + H) ↔ Quotient.mk setoid (G + H) = Quotient.mk setoid 0
[PROOFSTEP]
exact ⟨Eq.symm, Eq.symm⟩
[GOAL]
G✝ : PGame
inst✝¹ : Impartial G✝
G : PGame
inst✝ : Impartial G
⊢ G ≤ 0 ↔ 0 ≤ G
[PROOFSTEP]
rw [← zero_le_neg_iff, le_congr_right (neg_equiv_self G)]
[GOAL]
G✝ : PGame
inst✝¹ : Impartial G✝
G : PGame
inst✝ : Impartial G
⊢ G ⧏ 0 ↔ 0 ⧏ G
[PROOFSTEP]
rw [← zero_lf_neg_iff, lf_congr_right (neg_equiv_self G)]
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ (∀ (i : LeftMoves G), moveLeft G i ‖ 0) ↔ G ≈ 0
[PROOFSTEP]
refine' ⟨fun hb => _, fun hp i => _⟩
[GOAL]
case refine'_1
G : PGame
inst✝ : Impartial G
hb : ∀ (i : LeftMoves G), moveLeft G i ‖ 0
⊢ G ≈ 0
[PROOFSTEP]
rw [equiv_zero_iff_le G, le_zero_lf]
[GOAL]
case refine'_1
G : PGame
inst✝ : Impartial G
hb : ∀ (i : LeftMoves G), moveLeft G i ‖ 0
⊢ ∀ (i : LeftMoves G), moveLeft G i ⧏ 0
[PROOFSTEP]
exact fun i => (hb i).1
[GOAL]
case refine'_2
G : PGame
inst✝ : Impartial G
hp : G ≈ 0
i : LeftMoves G
⊢ moveLeft G i ‖ 0
[PROOFSTEP]
rw [fuzzy_zero_iff_lf]
[GOAL]
case refine'_2
G : PGame
inst✝ : Impartial G
hp : G ≈ 0
i : LeftMoves G
⊢ moveLeft G i ⧏ 0
[PROOFSTEP]
exact hp.1.moveLeft_lf i
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ (∀ (j : RightMoves G), moveRight G j ‖ 0) ↔ G ≈ 0
[PROOFSTEP]
refine' ⟨fun hb => _, fun hp i => _⟩
[GOAL]
case refine'_1
G : PGame
inst✝ : Impartial G
hb : ∀ (j : RightMoves G), moveRight G j ‖ 0
⊢ G ≈ 0
[PROOFSTEP]
rw [equiv_zero_iff_ge G, zero_le_lf]
[GOAL]
case refine'_1
G : PGame
inst✝ : Impartial G
hb : ∀ (j : RightMoves G), moveRight G j ‖ 0
⊢ ∀ (j : RightMoves G), 0 ⧏ moveRight G j
[PROOFSTEP]
exact fun i => (hb i).2
[GOAL]
case refine'_2
G : PGame
inst✝ : Impartial G
hp : G ≈ 0
i : RightMoves G
⊢ moveRight G i ‖ 0
[PROOFSTEP]
rw [fuzzy_zero_iff_gf]
[GOAL]
case refine'_2
G : PGame
inst✝ : Impartial G
hp : G ≈ 0
i : RightMoves G
⊢ 0 ⧏ moveRight G i
[PROOFSTEP]
exact hp.2.lf_moveRight i
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ (∃ i, moveLeft G i ≈ 0) ↔ G ‖ 0
[PROOFSTEP]
refine' ⟨fun ⟨i, hi⟩ => (fuzzy_zero_iff_gf G).2 (lf_of_le_moveLeft hi.2), fun hn => _⟩
[GOAL]
G : PGame
inst✝ : Impartial G
hn : G ‖ 0
⊢ ∃ i, moveLeft G i ≈ 0
[PROOFSTEP]
rw [fuzzy_zero_iff_gf G, zero_lf_le] at hn 
[GOAL]
G : PGame
inst✝ : Impartial G
hn : ∃ i, 0 ≤ moveLeft G i
⊢ ∃ i, moveLeft G i ≈ 0
[PROOFSTEP]
cases' hn with i hi
[GOAL]
case intro
G : PGame
inst✝ : Impartial G
i : LeftMoves G
hi : 0 ≤ moveLeft G i
⊢ ∃ i, moveLeft G i ≈ 0
[PROOFSTEP]
exact ⟨i, (equiv_zero_iff_ge _).2 hi⟩
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ (∃ j, moveRight G j ≈ 0) ↔ G ‖ 0
[PROOFSTEP]
refine' ⟨fun ⟨i, hi⟩ => (fuzzy_zero_iff_lf G).2 (lf_of_moveRight_le hi.1), fun hn => _⟩
[GOAL]
G : PGame
inst✝ : Impartial G
hn : G ‖ 0
⊢ ∃ j, moveRight G j ≈ 0
[PROOFSTEP]
rw [fuzzy_zero_iff_lf G, lf_zero_le] at hn 
[GOAL]
G : PGame
inst✝ : Impartial G
hn : ∃ j, moveRight G j ≤ 0
⊢ ∃ j, moveRight G j ≈ 0
[PROOFSTEP]
cases' hn with i hi
[GOAL]
case intro
G : PGame
inst✝ : Impartial G
i : RightMoves G
hi : moveRight G i ≤ 0
⊢ ∃ j, moveRight G j ≈ 0
[PROOFSTEP]
exact ⟨i, (equiv_zero_iff_le _).2 hi⟩
