rw [List.length_replicate, List.length_replicate, of_digits_zeros_eq_zero, zero_add]
b m n : ℕ
⊢ Nat.ofDigits b (List.replicate m 1) + b ^ (List.replicate m 1).length * Nat.ofDigits b (List.replicate n 1) =
    Nat.ofDigits b (List.replicate m 1) +
      (Nat.ofDigits b (List.replicate m 0) + b ^ (List.replicate m 0).length * Nat.ofDigits b (List.replicate n 1))
no goals