have not_two_le : ¬2 ≤ (i * i + i) % 2 := by
  cases Nat.mod_two_eq_zero_or_one (i * i + i) <;> simp [*]
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ (i * i + i) / 2 + i + 1 =
    ((i * i + i + i + i) / 2 + if 2 ∣ Nat.succ (i * i + i + i + i) then 1 else 0) +
      if 2 ∣ Nat.succ (Nat.succ (i * i + i + i + i)) then 1 else 0
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ (i * i + i) / 2 + i + 1 =
    ((i * i + i + i + i) / 2 + if 2 ∣ Nat.succ (i * i + i + i + i) then 1 else 0) +
      if 2 ∣ Nat.succ (Nat.succ (i * i + i + i + i)) then 1 else 0