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))
x : ℕ
hx : x ∈ Finset.range 1319 ∧ ¬Even x
h9 : (-1) ^ x = -1
⊢ -(1 / (↑x + 1)) = -1 / (↑x + 1)
no goals