Theorem: sum_id (LeanCourse/Lectures/Lecture7.lean)

State before:
n : ℕ
⊢ ∑ i in Finset.range (n + 1), i = n * (n + 1) / 2
Tactic:
symm
State after:
n : ℕ
⊢ n * (n + 1) / 2 = ∑ i in Finset.range (n + 1), i

State before:
n : ℕ
⊢ n * (n + 1) / 2 = ∑ i in Finset.range (n + 1), i
Tactic:
rw [Nat.div_eq_of_eq_mul_left]
State after:
case H1
n : ℕ
⊢ 0 < 2

case H2
n : ℕ
⊢ n * (n + 1) = (∑ i in Finset.range (n + 1), i) * 2

State before:
case H1
n : ℕ
⊢ 0 < 2

case H2
n : ℕ
⊢ n * (n + 1) = (∑ i in Finset.range (n + 1), i) * 2
Tactic:
norm_num
State after:
case H2
n : ℕ
⊢ n * (n + 1) = (∑ i in Finset.range (n + 1), i) * 2

State before:
case H2
n : ℕ
⊢ n * (n + 1) = (∑ i in Finset.range (n + 1), i) * 2
Tactic:
symm
State after:
case H2
n : ℕ
⊢ (∑ i in Finset.range (n + 1), i) * 2 = n * (n + 1)

State before:
case H2
n : ℕ
⊢ (∑ i in Finset.range (n + 1), i) * 2 = n * (n + 1)
Tactic:
induction n
State after:
case H2.zero

⊢ (∑ i in Finset.range (0 + 1), i) * 2 = 0 * (0 + 1)

case H2.succ
n✝ : ℕ
a✝ : (∑ i in Finset.range (n✝ + 1), i) * 2 = n✝ * (n✝ + 1)
⊢ (∑ i in Finset.range (n✝ + 1 + 1), i) * 2 = (n✝ + 1) * (n✝ + 1 + 1)

State before:
⊢ (∑ i in Finset.range (0 + 1), i) * 2 = 0 * (0 + 1)
Tactic:
case zero => simp
State after:
no goals

State before:
k : ℕ
ih : (∑ i in Finset.range (k + 1), i) * 2 = k * (k + 1)
⊢ (∑ i in Finset.range (k + 1 + 1), i) * 2 = (k + 1) * (k + 1 + 1)
Tactic:
case succ k ih =>
  rw [sum_range_succ, add_mul, ih]
  ring
State after:
no goals

State before:
⊢ (∑ i in Finset.range (0 + 1), i) * 2 = 0 * (0 + 1)
Tactic:
simp
State after:
no goals

State before:
k : ℕ
ih : (∑ i in Finset.range (k + 1), i) * 2 = k * (k + 1)
⊢ (∑ i in Finset.range (k + 1 + 1), i) * 2 = (k + 1) * (k + 1 + 1)
Tactic:
rw [sum_range_succ, add_mul, ih]
State after:
k : ℕ
ih : (∑ i in Finset.range (k + 1), i) * 2 = k * (k + 1)
⊢ k * (k + 1) + (k + 1) * 2 = (k + 1) * (k + 1 + 1)

State before:
k : ℕ
ih : (∑ i in Finset.range (k + 1), i) * 2 = k * (k + 1)
⊢ k * (k + 1) + (k + 1) * 2 = (k + 1) * (k + 1 + 1)
Tactic:
ring
State after:
no goals