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

State before:
M n : ℕ
X : GameState n
h : (init M n).IsReachable X
h0 : X.Ends
⊢ X.numMoves % 2 = M / n.succ % 2
Tactic:
have h1 := isReachable_central_card_add_numMoves_mod_two h
State after:
M n : ℕ
X : GameState n
h : (init M n).IsReachable X
h0 : X.Ends
h1 : (X.centralCards.card + X.numMoves) % 2 = ((init M n).centralCards.card + (init M n).numMoves) % 2
⊢ X.numMoves % 2 = M / n.succ % 2

State before:
M n : ℕ
X : GameState n
h : (init M n).IsReachable X
h0 : X.Ends
h1 : (X.centralCards.card + X.numMoves) % 2 = ((init M n).centralCards.card + (init M n).numMoves) % 2
⊢ X.numMoves % 2 = M / n.succ % 2
Tactic:
rwa [filter_central_init_card, numMoves_init, Nat.add_zero,
  filter_central_ends h0, card_empty, Nat.zero_add] at h1
State after:
no goals