rintro ⟨ha1, ha2⟩
case a.mpr
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 < 1319 ∧ ¬Even a → ∃ a_2 ∈ Finset.range 659, 2 * a_2 + 1 = a
case a.mpr.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 : ℕ
ha1 : a < 1319
ha2 : ¬Even a
⊢ ∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a