rw [←h2]
h2 :
  ∑ x ∈ Finset.filter (fun x => Even x) (Finset.range 1319), 1 / (↑x + 1) +
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1) =
    ∑ x ∈ Finset.range 1319, 1 / (↑x + 1)
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.range 1319, 1 / (↑i + 1) - 2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
h2 :
  ∑ x ∈ Finset.filter (fun x => Even x) (Finset.range 1319), 1 / (↑x + 1) +
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1) =
    ∑ x ∈ Finset.range 1319, 1 / (↑x + 1)
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ x ∈ Finset.filter (fun x => Even x) (Finset.range 1319), 1 / (↑x + 1) +
        ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))