Theorem: sum_id (LeanCourse/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean)

State before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ ∑ i in range (n + 1), i = n * (n + 1) / 2
Tactic:
symm
State after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) / 2 = ∑ i in range (n + 1), i

State before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) / 2 = ∑ i in range (n + 1), i
Tactic:
apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
State after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) = 2 * ∑ i in range (n + 1), i

State before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) = 2 * ∑ i in range (n + 1), i
Tactic:
induction' n with n ih
State after:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) = 2 * ∑ i in range (0 + 1), i

case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i in range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = 2 * ∑ i in range (n + 1 + 1), i

State before:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i in range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = 2 * ∑ i in range (n + 1 + 1), i
Tactic:
rw [Finset.sum_range_succ, mul_add 2, ← ih]
State after:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i in range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = n * (n + 1) + 2 * (n + 1)

State before:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i in range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = n * (n + 1) + 2 * (n + 1)
Tactic:
ring
State after:
no goals

State before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) = 2 * ∑ i in range (0 + 1), i
Tactic:
simp
State after:
no goals