rw [Nat.digits_def' (by norm_num) (by positivity)]
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ (Nat.digits 10 ((x + 1) * (10 ^ m * 10))).sum = (Nat.digits 10 (x + 1)).sum
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ ((x + 1) * (10 ^ m * 10) % 10 :: Nat.digits 10 ((x + 1) * (10 ^ m * 10) / 10)).sum = (Nat.digits 10 (x + 1)).sum