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

State before:
n : ℕ
X Y : GameState n
h : X.ValidMove Y
⊢ { ofColex := Y.board } < { ofColex := X.board }
Tactic:
rcases h with ⟨i, h⟩
State after:
case flip
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ { ofColex := { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board } <
    { ofColex := X.board }

State before:
case flip
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ { ofColex := { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board } <
    { ofColex := X.board }
Tactic:
refine Colex.toColex_lt_toColex.mpr ⟨?_, λ j h0 h1 ↦ ?_⟩
State after:
case flip.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board ≠ X.board

case flip.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
⊢ ∃ b ∈ X.board, b ∉ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board ∧ j ≤ b

State before:
case flip.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board ≠ X.board
Tactic:
rw [Ne, symmDiff_eq_left]
State after:
case flip.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ ¬Icc i (i + n) = ⊥

State before:
case flip.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ ¬Icc i (i + n) = ⊥
Tactic:
exact ne_empty_of_mem (left_mem_Icc.mpr le_self_add)
State after:
no goals

State before:
case flip.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
⊢ ∃ b ∈ X.board, b ∉ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board ∧ j ≤ b
Tactic:
refine ⟨i + n, h, λ h2 ↦ ?_, ?_⟩
State after:
case flip.refine_2.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
h2 : i + n ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
⊢ False

case flip.refine_2.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
⊢ j ≤ i + n

State before:
case flip.refine_2.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
h2 : i + n ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
⊢ False
Tactic:
rw [mem_symmDiff, mem_Icc] at h2
State after:
case flip.refine_2.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
h2 : i + n ∈ X.board ∧ ¬(i ≤ i + n ∧ i + n ≤ i + n) ∨ (i ≤ i + n ∧ i + n ≤ i + n) ∧ i + n ∉ X.board
⊢ False

State before:
case flip.refine_2.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
h2 : i + n ∈ X.board ∧ ¬(i ≤ i + n ∧ i + n ≤ i + n) ∨ (i ≤ i + n ∧ i + n ≤ i + n) ∧ i + n ∉ X.board
⊢ False
Tactic:
exact h2.elim (λ h2 ↦ h2.2 ⟨le_self_add, (i + n).le_refl⟩) (λ h2 ↦ h2.2 h)
State after:
no goals

State before:
case flip.refine_2.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
⊢ j ≤ i + n
Tactic:
rw [mem_symmDiff, or_iff_right (λ h2 ↦ h1 h2.1), mem_Icc] at h0
State after:
case flip.refine_2.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : (i ≤ j ∧ j ≤ i + n) ∧ j ∉ X.board
h1 : j ∉ X.board
⊢ j ≤ i + n

State before:
case flip.refine_2.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : (i ≤ j ∧ j ≤ i + n) ∧ j ∉ X.board
h1 : j ∉ X.board
⊢ j ≤ i + n
Tactic:
exact h0.1.2
State after:
no goals