let g i := f (n + m + i)
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + m + (m - 1 - x))
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
g : ℕ → ℚ := fun i => f (n + m + i)
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + m + (m - 1 - x))