dsimp only
b m n : ℕ
⊢ (let k := m + n;
    Nat.ofDigits b (List.replicate k 1)) =
    (let k := m;
      Nat.ofDigits b (List.replicate k 1)) +
      Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)
b m n : ℕ
⊢ Nat.ofDigits b (List.replicate (m + n) 1) =
    Nat.ofDigits b (List.replicate m 1) + Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)