clear h1
n m : ℕ
f : ℕ → ℚ
h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
⊢ ∑ 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 : ℕ → ℚ
⊢ ∑ 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)))