induction' m with m ih
m : ℕ
⊢ (Nat.digits 10 (10 ^ m)).length = m + 1
case zero

⊢ (Nat.digits 10 (10 ^ 0)).length = 0 + 1

case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ (m + 1))).length = m + 1 + 1