have h10 : ∑ 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 / ((x:ℚ) + 1) := by
  apply Finset.sum_congr rfl
  intro x hx
  rw [Finset.mem_filter] at hx
  have h9: (-1 : ℚ)^x = -1 := Odd.neg_one_pow (Nat.odd_iff_not_even.mpr hx.2)
  rw [h9]
  field_simp
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)
g : ℕ ↪ ℕ := { toFun := fun x => 2 * x + 1, inj' := ⋯ }
h4 : Finset.map g (Finset.range 659) = Finset.filter (fun x => ¬Even x) (Finset.range 1319)
h5 : ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1)) = ∑ i ∈ Finset.range 659, 1 / (↑(g i) + 1)
h6 : ∑ x ∈ Finset.map g (Finset.range 659), 1 / (↑x + 1) = ∑ x ∈ Finset.range 659, 1 / (↑(g x) + 1)
h3 :
  ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1) = ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1) +
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), -(1 / (↑x + 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)
g : ℕ ↪ ℕ := { toFun := fun x => 2 * x + 1, inj' := ⋯ }
h4 : Finset.map g (Finset.range 659) = Finset.filter (fun x => ¬Even x) (Finset.range 1319)
h5 : ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1)) = ∑ i ∈ Finset.range 659, 1 / (↑(g i) + 1)
h6 : ∑ x ∈ Finset.map g (Finset.range 659), 1 / (↑x + 1) = ∑ x ∈ Finset.range 659, 1 / (↑(g x) + 1)
h3 :
  ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1) = ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
h10 :
  ∑ 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 / (↑x + 1)
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1) +
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), -(1 / (↑x + 1))