simp [sumTo]
case succ
n : ℕ
ih : 2 * sumTo n = n * (n + 1)
⊢ 2 * sumTo (Nat.succ n) = Nat.succ n * (Nat.succ n + 1)
case succ
n : ℕ
ih : 2 * sumTo n = n * (n + 1)
⊢ 2 * (n + 1 + sumTo n) = Nat.succ n * (Nat.succ n + 1)