Simple induction proof

Stream: new members

[André Beyer]

I'm struggling to complete this simple inductive proof below:

example (n i : ℕ) : 2 * (∑ k in finset.range n, i) = n * (n + 1) :=
begin
  induction n with d hd,
  { simp, },
  {
    rw [← nat.add_one, finset.sum_range_succ, mul_add, hd],
    simp,
    sorry,
  }
end

I'll end up at the following state:

2 * i + d * (d + 1) = (d + 1) * (d + 2)

I'm particularly confused about finset.sum_range_succ. I was expecting to get d + 1 instead of i. Thanks in advance!

[Shing Tak Lam]

Is the statement correct? What you have is $2\sum_{k=0}^{n-1} i = n(n+1)$, not $2\sum_{k=0}^{n} k = n(n+1)$ (which is ∑ k in finset.range n.succ, k)

[André Beyer]

Right - embarrassingly. Thanks!

I'm still stuck after correction:

2 * d + d * (d + 1) = (d + 1) * (d + 2)

What would easily work is:

2 * (d + 1) + d * (d + 1) = (d + 1) * (d + 2)

I still don't understand why it's d and not d+1.

[Bryan Gin-ge Chen]

The i in the sum should be a k (and then i can be removed completely):

import algebra.big_operators.basic
import tactic

open_locale big_operators
example (n : ℕ) : 2 * (∑ k in finset.range (n + 1), k) = n * (n + 1) :=
begin
  induction n with d hd,
  { simp, },
  { rw [← nat.add_one, finset.sum_range_succ, mul_add, hd],
    ring, }
end

[André Beyer]

Thanks, that works.

I still have problems understanding it though. I wanted to proof

$$2 \cdot \sum_{k=1}^n k = n (n + 1)$$

I would translate the working version as follows though:

$$2 \cdot \sum_{k=1}^{n+1} k = n (n + 1)$$

In what range does finset.range operate? Is it usually from 0 to n-1 and thus we'd write n + 1?

[Bryan Gin-ge Chen]

finset.range n is the finite set of numbers $\{0,1,2,\dots,n-1\}$ (cf. docs#finset.range), so the sum in my code (2 * (∑ k in finset.range (n + 1), k)) translates to:

$$2 \cdot \sum_{k=0}^n k = n (n + 1)$$

[André Beyer]

Nice, thank you!