obtain ⟨k, hk⟩ := Nat.le.dest h3
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
⊢ ∃ k, k + (Nat.digits 10 y).length = m
case intro
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : (Nat.digits 10 y).length + k = m
⊢ ∃ k, k + (Nat.digits 10 y).length = m