rw [Finset.mem_range] at hi
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i ∈ Finset.range m
⊢ f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i < m
⊢ f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))