Theorem: Nat.todigitsCore_accumulates_suffix (One.lean)

State before:
b f n : ℕ
rest : List Char
⊢ toDigitsCore b f n rest = toDigitsCore b f n [] ++ rest
Tactic:
have h: rest = [] ++ rest := by simp
State after:
b f n : ℕ
rest : List Char
h : rest = [] ++ rest
⊢ toDigitsCore b f n rest = toDigitsCore b f n [] ++ rest

State before:
b f n : ℕ
rest : List Char
h : rest = [] ++ rest
⊢ toDigitsCore b f n rest = toDigitsCore b f n [] ++ rest
Tactic:
conv=> left; rw [h]
State after:
b f n : ℕ
rest : List Char
h : rest = [] ++ rest
⊢ toDigitsCore b f n ([] ++ rest) = toDigitsCore b f n [] ++ rest

State before:
b f n : ℕ
rest : List Char
h : rest = [] ++ rest
⊢ toDigitsCore b f n ([] ++ rest) = toDigitsCore b f n [] ++ rest
Tactic:
apply Nat.toDigitsCore_accumulates
State after:
no goals

State before:
b f n : ℕ
rest : List Char
⊢ rest = [] ++ rest
Tactic:
simp
State after:
no goals