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