case zero
R : Type ?u.168155
⊢ ∑ m in range (zero + 1), (-1) ^ m * ↑(Nat.choose zero m) = if zero = 0 then 1 else 0

case succ
R : Type ?u.168155
n✝ : ℕ
⊢ ∑ m in range (Nat.succ n✝ + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n✝) m) = if Nat.succ n✝ = 0 then 1 else 0
R : Type ?u.168155
n : ℕ
⊢ ∑ m in range (n + 1), (-1) ^ m * ↑(Nat.choose n m) = if n = 0 then 1 else 0
cases n
no goals
case succ
R : Type ?u.168155
n✝ : ℕ
⊢ ∑ m in range (Nat.succ n✝ + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n✝) m) = if Nat.succ n✝ = 0 then 1 else 0
case succ n =>
  have h := add_pow (-1 : ℤ) 1 n.succ
  simp only [one_pow, mul_one, add_left_neg] at h
  rw [← h, zero_pow (Nat.succ_pos n), if_neg (Nat.succ_ne_zero n)]
no goals
case zero
R : Type ?u.168155
⊢ ∑ m in range (zero + 1), (-1) ^ m * ↑(Nat.choose zero m) = if zero = 0 then 1 else 0
simp
R : Type ?u.168155
n : ℕ
h :
  (-1 + 1) ^ Nat.succ n = ∑ m in range (Nat.succ n + 1), (-1) ^ m * 1 ^ (Nat.succ n - m) * ↑(Nat.choose (Nat.succ n) m)
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
R : Type ?u.168155
n : ℕ
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
have h := add_pow (-1 : ℤ) 1 n.succ
R : Type ?u.168155
n : ℕ
h : 0 ^ Nat.succ n = ∑ x in range (Nat.succ n + 1), (-1) ^ x * ↑(Nat.choose (Nat.succ n) x)
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
R : Type ?u.168155
n : ℕ
h :
  (-1 + 1) ^ Nat.succ n = ∑ m in range (Nat.succ n + 1), (-1) ^ m * 1 ^ (Nat.succ n - m) * ↑(Nat.choose (Nat.succ n) m)
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
simp only [one_pow, mul_one, add_left_neg] at h
no goals
R : Type ?u.168155
n : ℕ
h : 0 ^ Nat.succ n = ∑ x in range (Nat.succ n + 1), (-1) ^ x * ↑(Nat.choose (Nat.succ n) x)
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
rw [← h, zero_pow (Nat.succ_pos n), if_neg (Nat.succ_ne_zero n)]