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

State before:
b m : ℕ
⊢ Nat.ofDigits b (List.replicate m 0) = 0
Tactic:
induction' m with m ih
State after:
case zero
b : ℕ
⊢ Nat.ofDigits b (List.replicate 0 0) = 0

case succ
b m : ℕ
ih : Nat.ofDigits b (List.replicate m 0) = 0
⊢ Nat.ofDigits b (List.replicate (m + 1) 0) = 0

State before:
case zero
b : ℕ
⊢ Nat.ofDigits b (List.replicate 0 0) = 0
Tactic:
rfl
State after:
no goals

State before:
case succ
b m : ℕ
ih : Nat.ofDigits b (List.replicate m 0) = 0
⊢ Nat.ofDigits b (List.replicate (m + 1) 0) = 0
Tactic:
simp only [Nat.ofDigits, Nat.cast_zero, ih, mul_zero, add_zero]
State after:
no goals