How to prove the sum of cubes formula in Lean 4?

Stream: new members

[decade_g]

import Mathlib
-- 1³ + 2³ + ... + n³ = (n(n+1)/2)²
lemma sum_cubes (i:ℕ) :∑ j ∈ Finset.Icc 1 i, (j:ℝ)^3 = ((i * (i + 1)) / 2)^2 := by
  sorry

[Kenny Lau]

As always, the advice is to try to prove it on paper first.

[decade_g]

Kenny Lau 发言道：

As always, the advice is to try to prove it on paper first.

I might not have expressed my question clearly. What I meant to ask is whether there is a directly usable theorem in mathlib. I tried exact? but didn’t get an answer.

[Kenny Lau]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Bernoulli.html#sum_range_pow

[Kenny Lau]

there's this for sum of powers in general

[Kenny Lau]

decade_g said:

I might not have expressed my question clearly. What I meant to ask is whether there is a directly usable theorem in mathlib. I tried exact? but didn’t get an answer.

You might want to ask this in #Is there code for X? next time