Theorem: Nat.toDigits_length_eq_log (One.lean)

State before:
b n : ℕ
P : b > 1
⊢ List.length (toDigits b n) = log b n + 1
Tactic:
unfold Nat.toDigits
State after:
b n : ℕ
P : b > 1
⊢ List.length (toDigitsCore b (n + 1) n []) = log b n + 1

State before:
b n : ℕ
P : b > 1
⊢ List.length (toDigitsCore b (n + 1) n []) = log b n + 1
Tactic:
rw [Nat.toDigitsCore_length_eq_log]
State after:
b n : ℕ
P : b > 1
⊢ log b n + 1 + List.length [] = log b n + 1

case P
b n : ℕ
P : b > 1
⊢ b > 1

case R
b n : ℕ
P : b > 1
⊢ n + 1 > n

State before:
b n : ℕ
P : b > 1
⊢ log b n + 1 + List.length [] = log b n + 1

case P
b n : ℕ
P : b > 1
⊢ b > 1

case R
b n : ℕ
P : b > 1
⊢ n + 1 > n
Tactic:
. simp only [List.length_nil, add_zero]
State after:
case P
b n : ℕ
P : b > 1
⊢ b > 1

case R
b n : ℕ
P : b > 1
⊢ n + 1 > n

State before:
case P
b n : ℕ
P : b > 1
⊢ b > 1

case R
b n : ℕ
P : b > 1
⊢ n + 1 > n
Tactic:
. exact P
State after:
case R
b n : ℕ
P : b > 1
⊢ n + 1 > n

State before:
case R
b n : ℕ
P : b > 1
⊢ n + 1 > n
Tactic:
. apply Nat.lt_succ_self
State after:
no goals