have h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i)) := by
  intro i hi
  rw [Finset.mem_range] at hi
  apply congr_arg
  omega
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
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 + (2 * m - 1 - x))