constructor
case h
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
r : ℕ
hr : a = 2 * r + 1
⊢ r ∈ Finset.range 659 ∧ 2 * r + 1 = a
case h.left
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
r : ℕ
hr : a = 2 * r + 1
⊢ r ∈ Finset.range 659

case h.right
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
r : ℕ
hr : a = 2 * r + 1
⊢ 2 * r + 1 = a