Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
b : ℕ
P : b > 1
accum : List Char
heq✝ : accum = [] ++ accum
n w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > n
heq : ¬n / b = 0
h : n / b < n
⊢ log b (n / b) + 1 = log b n

case a
b : ℕ
P : b > 1
accum : List Char
heq✝ : accum = [] ++ accum
n w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > n
heq : ¬n / b = 0
h : n / b < n
⊢ n / b < n

case accum
b : ℕ
P : b > 1
accum : List Char
heq✝ : accum = [] ++ accum
n w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > n
heq : ¬n / b = 0
h : n / b < n
⊢ List Char

case R
b : ℕ
P : b > 1
accum : List Char
heq✝ : accum = [] ++ accum
n w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > n
heq : ¬n / b = 0
h : n / b < n
⊢ l > n / b

case heq
b : ℕ
P : b > 1
accum : List Char
heq✝ : accum = [] ++ accum
n w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > n
heq : ¬n / b = 0
h : n / b < n
⊢ ?accum = [] ++ ?accum
Tactic:
. rw [Nat.log_div_base, Nat.sub_add_cancel]
  apply Nat.log_pos
  . apply P
  . apply (Nat.one_le_div_iff (Nat.lt_of_succ_lt P)).1
    apply Nat.succ_le_iff.2
    apply Nat.pos_of_ne_zero
    apply heq
Proof state after:
case a
b : ℕ
P : b > 1
accum : List Char
heq✝ : accum = [] ++ accum
n w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > n
heq : ¬n / b = 0
h : n / b < n
⊢ n / b < n

case accum
b : ℕ
P : b > 1
accum : List Char
heq✝ : accum = [] ++ accum
n w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > n
heq : ¬n / b = 0
h : n / b < n
⊢ List Char

case R
b : ℕ
P : b > 1
accum : List Char
heq✝ : accum = [] ++ accum
n w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > n
heq : ¬n / b = 0
h : n / b < n
⊢ l > n / b

case heq
b : ℕ
P : b > 1
accum : List Char
heq✝ : accum = [] ++ accum
n w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > n
heq : ¬n / b = 0
h : n / b < n
⊢ ?accum = [] ++ ?accum