have ⟨k, hk⟩ : ∃ k, k + (Nat.digits 10 y).length = m := by
  obtain ⟨k, hk⟩ := Nat.le.dest h3
  rw [add_comm] at hk
  exact ⟨k, hk⟩
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m + y)).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m + y)).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum