case zero
α : Type u
inst✝ : Ring α
⊢ ∑ i in range Nat.zero, (-1) ^ i = if Even Nat.zero then 0 else 1

case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
⊢ ∑ i in range (Nat.succ k), (-1) ^ i = if Even (Nat.succ k) then 0 else 1
α : Type u
inst✝ : Ring α
n : ℕ
⊢ ∑ i in range n, (-1) ^ i = if Even n then 0 else 1
induction' n with k hk
no goals
case zero
α : Type u
inst✝ : Ring α
⊢ ∑ i in range Nat.zero, (-1) ^ i = if Even Nat.zero then 0 else 1
simp
case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
⊢ ((-1) ^ k + if Even k then 0 else 1) = if ¬Even k then 0 else 1
case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
⊢ ∑ i in range (Nat.succ k), (-1) ^ i = if Even (Nat.succ k) then 0 else 1
simp only [geom_sum_succ', Nat.even_add_one, hk]
case succ.inl
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
h : Even k
⊢ (-1) ^ k + 0 = 1

case succ.inr
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0
case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
⊢ ((-1) ^ k + if Even k then 0 else 1) = if ¬Even k then 0 else 1
split_ifs with h
no goals
case succ.inl
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
h : Even k
⊢ (-1) ^ k + 0 = 1
rw [h.neg_one_pow, add_zero]
no goals
case succ.inr
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0
rw [(Nat.odd_iff_not_even.2 h).neg_one_pow, neg_add_self]