simp only [sumDrop, powers, pow_three, 
  dropEveryNth_eq_fun, pnats, Nat.div_one,
  sum_eq_three_even
]
case h
i : ℕ
⊢ sumDrop 3 pnats i = powers 3 i
case h
i : ℕ
⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))