Theorem: ZerosOnesAndTwos.ones_add (Compfiles/ZeroesOnesAndTwos.lean)

State before:
b m n : ℕ
⊢ ones b (m + n) = ones b m + Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)
Tactic:
unfold ones
State after:
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)

State before:
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)
Tactic:
dsimp only
State after:
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)

State before:
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)
Tactic:
rw [List.replicate_add, Nat.ofDigits_append, Nat.ofDigits_append]
State after:
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))

State before:
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))
Tactic:
rw [List.length_replicate, List.length_replicate, of_digits_zeros_eq_zero, zero_add]
State after:
no goals