rw [Finset.mem_range] at hb1
case a.mp.intro.intro
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 b : ℕ
hb1 : b ∈ Finset.range 659
hb2 : 2 * b + 1 = a
⊢ a < 1319 ∧ ¬Even a
case a.mp.intro.intro
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 b : ℕ
hb1 : b < 659
hb2 : 2 * b + 1 = a
⊢ a < 1319 ∧ ¬Even a