Theorem: Usa1985P1.nicomachus' (Compfiles/Usa1985P1.lean)

State before:
n : ℕ
⊢ ∑ i ∈ Finset.range n, (↑i + 1) ^ 3 = (∑ i ∈ Finset.range n, (↑i + 1)) ^ 2
Tactic:
norm_cast
State after:
n : ℕ
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2

State before:
n : ℕ
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2
Tactic:
have h1 := nicomachus (n + 1)
State after:
n : ℕ
h1 : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2

State before:
n : ℕ
h1 : ∑ i ∈ Finset.range (n + 1), i ^ 3 = (∑ i ∈ Finset.range (n + 1), i) ^ 2
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2
Tactic:
simp only [Finset.sum_range_succ', zero_pow, add_zero] at h1
State after:
n : ℕ
h1 : ∑ k ∈ Finset.range n, (k + 1) ^ 3 + 0 ^ 3 = (∑ k ∈ Finset.range n, (k + 1)) ^ 2
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2

State before:
n : ℕ
h1 : ∑ k ∈ Finset.range n, (k + 1) ^ 3 + 0 ^ 3 = (∑ k ∈ Finset.range n, (k + 1)) ^ 2
⊢ ∑ x ∈ Finset.range n, (x + 1) ^ 3 = (∑ x ∈ Finset.range n, (x + 1)) ^ 2
Tactic:
exact h1
State after:
no goals