Theorem: IMOSL.IMO2017C1.sum_neg_one_pow_Ico (IMOSLLean4/IMO2017/C1/C1.lean)

State before:
a : ℕ
⊢ ∑ x ∈ Ico a (a + 0), (-1) ^ x = bif Nat.bodd 0 then (-1) ^ a else 0
Tactic:
rw [add_zero, Ico_self]
State after:
a : ℕ
⊢ ∑ x ∈ ∅, (-1) ^ x = bif Nat.bodd 0 then (-1) ^ a else 0

State before:
a : ℕ
⊢ ∑ x ∈ ∅, (-1) ^ x = bif Nat.bodd 0 then (-1) ^ a else 0
Tactic:
rfl
State after:
no goals

State before:
a : ℕ
⊢ ∑ x ∈ Ico a (a + 1), (-1) ^ x = bif Nat.bodd 1 then (-1) ^ a else 0
Tactic:
rw [Nat.Ico_succ_singleton, sum_singleton]
State after:
a : ℕ
⊢ (-1) ^ a = bif Nat.bodd 1 then (-1) ^ a else 0

State before:
a : ℕ
⊢ (-1) ^ a = bif Nat.bodd 1 then (-1) ^ a else 0
Tactic:
rfl
State after:
no goals

State before:
a n : ℕ
⊢ ∑ x ∈ Ico a (a + (n + 2)), (-1) ^ x = bif (n + 2).bodd then (-1) ^ a else 0
Tactic:
have h : a ≤ a + n := a.le_add_right n
State after:
a n : ℕ
h : a ≤ a + n
⊢ ∑ x ∈ Ico a (a + (n + 2)), (-1) ^ x = bif (n + 2).bodd then (-1) ^ a else 0

State before:
a n : ℕ
h : a ≤ a + n
⊢ ∑ x ∈ Ico a (a + (n + 2)), (-1) ^ x = bif (n + 2).bodd then (-1) ^ a else 0
Tactic:
rw [← add_assoc, sum_Ico_succ_top (h.trans (a + n).le_succ),
  pow_succ', neg_one_mul, sum_Ico_succ_top h, sum_neg_one_pow_Ico a n,
  add_neg_cancel_right, Nat.bodd_add, Nat.bodd_two, Bool.xor_false]
State after:
no goals