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

State before:
n : ℕ
X Y : GameState n
h : X.IsReachable Y
a✝ c✝ : GameState n
h0 : a✝.ValidMove c✝
x✝ : ReflTransGen ValidMove c✝ Y
h1 : ∑ i ∈ Y.board, 2 ^ i + Y.numMoves ≤ ∑ i ∈ c✝.board, 2 ^ i + c✝.numMoves
⊢ ∑ i ∈ c✝.board, 2 ^ i + c✝.numMoves ≤ ∑ i ∈ a✝.board, 2 ^ i + a✝.numMoves
Tactic:
rw [ValidMove_numMoves h0, ← add_assoc, Nat.succ_le_iff]
State after:
n : ℕ
X Y : GameState n
h : X.IsReachable Y
a✝ c✝ : GameState n
h0 : a✝.ValidMove c✝
x✝ : ReflTransGen ValidMove c✝ Y
h1 : ∑ i ∈ Y.board, 2 ^ i + Y.numMoves ≤ ∑ i ∈ c✝.board, 2 ^ i + c✝.numMoves
⊢ ∑ i ∈ c✝.board, 2 ^ i + a✝.numMoves < ∑ i ∈ a✝.board, 2 ^ i + a✝.numMoves

State before:
n : ℕ
X Y : GameState n
h : X.IsReachable Y
a✝ c✝ : GameState n
h0 : a✝.ValidMove c✝
x✝ : ReflTransGen ValidMove c✝ Y
h1 : ∑ i ∈ Y.board, 2 ^ i + Y.numMoves ≤ ∑ i ∈ c✝.board, 2 ^ i + c✝.numMoves
⊢ ∑ i ∈ c✝.board, 2 ^ i + a✝.numMoves < ∑ i ∈ a✝.board, 2 ^ i + a✝.numMoves
Tactic:
exact Nat.add_lt_add_right (ValidMove_sum_two_pow h0) _
State after:
no goals