unfold_let g
case a
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' := ⋯ }
a : ℕ
⊢ a ∈ Finset.map g (Finset.range 659) ↔ a ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319)
case a
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' := ⋯ }
a : ℕ
⊢ a ∈ Finset.map { toFun := fun x => 2 * x + 1, inj' := ⋯ } (Finset.range 659) ↔
    a ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319)