Theorem: Nat.toDigits_zero (One.lean)

State before:
b : ℕ
⊢ toDigits b 0 = [Char.ofNat 48]
Tactic:
unfold toDigits toDigitsCore
State after:
b : ℕ
⊢ (let d := digitChar (0 % b);
    let n' := 0 / b;
    if n' = 0 then [d] else toDigitsCore b 0 n' [d]) =
    [Char.ofNat 48]

State before:
b : ℕ
⊢ (let d := digitChar (0 % b);
    let n' := 0 / b;
    if n' = 0 then [d] else toDigitsCore b 0 n' [d]) =
    [Char.ofNat 48]
Tactic:
simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.zero_div, zero_mod, ite_true, List.cons.injEq]
State after:
no goals