simp only [Finset.sum_Ico_eq_sum_range, add_tsub_cancel_left]
n m : ℕ
f : ℕ → ℚ
⊢ ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
n m : ℕ
f : ℕ → ℚ
⊢ ∑ x ∈ Finset.range m, f (n + x) + ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))