R : Type ?u.145590
n : ℕ
this : ∑ m in range (n + 1), 1 ^ m * 1 ^ (n - m) * ↑(choose n m) = (1 + 1) ^ n
⊢ ∑ m in range (n + 1), choose n m = 2 ^ n
R : Type ?u.145590
n : ℕ
⊢ ∑ m in range (n + 1), choose n m = 2 ^ n
have := (add_pow 1 1 n).symm
no goals
R : Type ?u.145590
n : ℕ
this : ∑ m in range (n + 1), 1 ^ m * 1 ^ (n - m) * ↑(choose n m) = (1 + 1) ^ n
⊢ ∑ m in range (n + 1), choose n m = 2 ^ n
simpa [one_add_one_eq_two] using this