How to make a "change of variables" in an infinite series?

Stream: new members

[spamegg]

import Mathlib

example : ∑' n : Set.Ici 5, ((1 : ℝ) / (n-4)^2) = ∑' n : ℕ, ((1 : ℝ) / (n+1)^2) := by sorry

[Weiyi Wang]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/InfiniteSum/Basic.html#Equiv.hasSum_iff
or its neighbors below can help