Theorem: Section15Sheet7Solutions.sum_fifths (FormalisingMathematics2024/Solutions/Section15numberTheory/Sheet7.lean)

State before:
n : ℕ
⊢ ∑ i in range n, ↑i ^ 5 = (4 * (↑n * (↑n - 1) / 2) ^ 3 - (↑n * (↑n - 1) / 2) ^ 2) / 3
Tactic:
induction' n with d hd
State after:
case zero

⊢ ∑ i in range Nat.zero, ↑i ^ 5 =
    (4 * (↑Nat.zero * (↑Nat.zero - 1) / 2) ^ 3 - (↑Nat.zero * (↑Nat.zero - 1) / 2) ^ 2) / 3

case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ ∑ i in range (Nat.succ d), ↑i ^ 5 =
    (4 * (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 3 - (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2) / 3

State before:
case zero

⊢ ∑ i in range Nat.zero, ↑i ^ 5 =
    (4 * (↑Nat.zero * (↑Nat.zero - 1) / 2) ^ 3 - (↑Nat.zero * (↑Nat.zero - 1) / 2) ^ 2) / 3
Tactic:
simp
State after:
no goals

State before:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ ∑ i in range (Nat.succ d), ↑i ^ 5 =
    (4 * (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 3 - (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2) / 3
Tactic:
rw [Finset.sum_range_succ, hd]
State after:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3 + ↑d ^ 5 =
    (4 * (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 3 - (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2) / 3

State before:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3 + ↑d ^ 5 =
    (4 * (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 3 - (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2) / 3
Tactic:
simp
State after:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ (4 * ((↑d * (↑d - 1)) ^ 3 / 2 ^ 3) - (↑d * (↑d - 1)) ^ 2 / 2 ^ 2) / 3 + ↑d ^ 5 =
    (4 * (((↑d + 1) * ↑d) ^ 3 / 2 ^ 3) - ((↑d + 1) * ↑d) ^ 2 / 2 ^ 2) / 3

State before:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ (4 * ((↑d * (↑d - 1)) ^ 3 / 2 ^ 3) - (↑d * (↑d - 1)) ^ 2 / 2 ^ 2) / 3 + ↑d ^ 5 =
    (4 * (((↑d + 1) * ↑d) ^ 3 / 2 ^ 3) - ((↑d + 1) * ↑d) ^ 2 / 2 ^ 2) / 3
Tactic:
ring
State after:
no goals