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

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

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

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

State before:
case zero

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

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

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

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