rw [←mul_left_comm]
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 2 * (10 * 10 ^ (Nat.digits 10 (n.succ / 10)).length)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 10 * (2 * 10 ^ (Nat.digits 10 (n.succ / 10)).length)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10