Theorem: IMOSL.IMO2009C1.GameState.Ends_iff (IMOSLLean4/IMO2009/C1/C1.lean)

State before:
n : ℕ
X : GameState n
h : X.Ends
i : ℕ
h0 : i ∈ X.board
⊢ i ∈ range n
Tactic:
rw [mem_range, ← not_le]
State after:
n : ℕ
X : GameState n
h : X.Ends
i : ℕ
h0 : i ∈ X.board
⊢ ¬n ≤ i

State before:
n : ℕ
X : GameState n
h : X.Ends
i : ℕ
h0 : i ∈ X.board
⊢ ¬n ≤ i
Tactic:
refine λ h1 ↦ h _ <| ValidMove.flip (i - n) ?_
State after:
n : ℕ
X : GameState n
h : X.Ends
i : ℕ
h0 : i ∈ X.board
h1 : n ≤ i
⊢ i - n + n ∈ X.board

State before:
n : ℕ
X : GameState n
h : X.Ends
i : ℕ
h0 : i ∈ X.board
h1 : n ≤ i
⊢ i - n + n ∈ X.board
Tactic:
rwa [Nat.sub_add_cancel h1]
State after:
no goals