internlm/Lean-Github huggingface dataset:
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case inr
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
x✝ w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < x✝ →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > x✝
h✝ : ¬x✝ / b = 0
⊢ List.length (toDigitsCore b l (x✝ / b) [digitChar (x✝ % b)]) = log b x✝ + 1
Tactic:
. next n heq =>
  rw [Nat.todigitsCore_accumulates_suffix]
  simp only [List.length_append, List.length_singleton, add_left_inj]
  have h: n/b<n := by
    apply Nat.div_lt_self
    . apply Nat.pos_of_ne_zero
      intro h
      simp only [h, Nat.zero_div, not_true] at heq
    . apply P
  rw [ih]
  . 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
  . exact h
  . exact []
  . calc
    l ≥ n := by exact le_of_lt_succ R
    _ > n/b := h
  . simp
Proof state after:
no goals
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > i
h₂ : i / b = 0
⊢ List.length [digitChar (i % b)] = log b i + 1
Tactic:
simp
Proof state after:
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > i
h₂ : i / b = 0
⊢ i < b ∨ b ≤ 1
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > i
h₂ : i / b = 0
⊢ i < b ∨ b ≤ 1
Tactic:
left
Proof state after:
case h
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > i
h₂ : i / b = 0
⊢ i < b
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case h
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > i
h₂ : i / b = 0
⊢ i < b
Tactic:
have  h: b > 0 := pos_of_gt P
Proof state after:
case h
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > i
h₂ : i / b = 0
h : b > 0
⊢ i < b
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case h
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > i
h₂ : i / b = 0
h : b > 0
⊢ i < b
Tactic:
apply (Nat.div_lt_one_iff h).1
Proof state after:
case h
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > i
h₂ : i / b = 0
h : b > 0
⊢ i / b < 1
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case h
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i w y : ℕ
p : List Char
l : ℕ
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ l > i
h₂ : i / b = 0
h : b > 0
⊢ i / b < 1
Tactic:
simp only [h₂, zero_lt_one]
Proof state after:
no goals
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
⊢ List.length (toDigitsCore b l (n / b) [digitChar (n % b)]) = log b n + 1
Tactic:
rw [Nat.todigitsCore_accumulates_suffix]
Proof state after:
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
⊢ List.length (toDigitsCore b l (n / b) [] ++ [digitChar (n % b)]) = log b n + 1
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
⊢ List.length (toDigitsCore b l (n / b) [] ++ [digitChar (n % b)]) = log b n + 1
Tactic:
simp only [List.length_append, List.length_singleton, add_left_inj]
Proof state after:
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
⊢ List.length (toDigitsCore b l (n / b) []) = log b n
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
⊢ List.length (toDigitsCore b l (n / b) []) = log b n
Tactic:
have h: n/b<n := by
  apply Nat.div_lt_self
  . apply Nat.pos_of_ne_zero
    intro h
    simp only [h, Nat.zero_div, not_true] at heq
  . apply P
Proof state after:
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.length (toDigitsCore b l (n / b) []) = log b n
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
⊢ List.length (toDigitsCore b l (n / b) []) = log b n
Tactic:
rw [ih]
Proof state after:
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
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
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:
. exact h
Proof state after:
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
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
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:
. exact []
Proof state after:
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
⊢ [] = [] ++ []
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
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
⊢ [] = [] ++ []
Tactic:
. calc
  l ≥ n := by exact le_of_lt_succ R
  _ > n/b := h
Proof state after:
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
⊢ [] = [] ++ []
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
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
⊢ [] = [] ++ []
Tactic:
. simp
Proof state after:
no goals
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
⊢ n / b < n
Tactic:
apply Nat.div_lt_self
Proof state after:
case hLtN
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
⊢ 0 < n

case hLtK
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
⊢ 1 < b
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case hLtN
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
⊢ 0 < n

case hLtK
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
⊢ 1 < b
Tactic:
. apply Nat.pos_of_ne_zero
  intro h
  simp only [h, Nat.zero_div, not_true] at heq
Proof state after:
case hLtK
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
⊢ 1 < b
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case hLtK
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
⊢ 1 < b
Tactic:
. apply P
Proof state after:
no goals
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
⊢ l ≥ n
Tactic:
exact le_of_lt_succ R
Proof state after:
no goals
Theorem: Nat.toDigits_length_eq_log
Proof state before:
b n : ℕ
P : b > 1
⊢ List.length (toDigits b n) = log b n + 1
Tactic:
unfold Nat.toDigits
Proof state after:
b n : ℕ
P : b > 1
⊢ List.length (toDigitsCore b (n + 1) n []) = log b n + 1
Theorem: Nat.toDigits_length_eq_log
Proof 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]
Proof 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
Theorem: Nat.toDigits_length_eq_log
Proof 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]
Proof state after:
case P
b n : ℕ
P : b > 1
⊢ b > 1

case R
b n : ℕ
P : b > 1
⊢ n + 1 > n
Theorem: Nat.toDigits_length_eq_log
Proof state before:
case P
b n : ℕ
P : b > 1
⊢ b > 1

case R
b n : ℕ
P : b > 1
⊢ n + 1 > n
Tactic:
. exact P
Proof state after:
case R
b n : ℕ
P : b > 1
⊢ n + 1 > n
Theorem: Nat.toDigits_length_eq_log
Proof state before:
case R
b n : ℕ
P : b > 1
⊢ n + 1 > n
Tactic:
. apply Nat.lt_succ_self
Proof state after:
no goals
Theorem: Nat.toDigits_eq_digit
Proof state before:
b n : ℕ
P : b > 1
⊢ ∀ (i : ℕ),
    i < List.length (toDigits b n) →
      List.getD (toDigits b n) i (Char.ofNat 48) = digitChar (digit b n (List.length (toDigits b n) - 1 - i))
Tactic:
intro i h
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.getD (toDigits b n) i (Char.ofNat 48) = digitChar (digit b n (List.length (toDigits b n) - 1 - i))
Theorem: Nat.toDigits_eq_digit
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.getD (toDigits b n) i (Char.ofNat 48) = digitChar (digit b n (List.length (toDigits b n) - 1 - i))
Tactic:
rw [← Nat.toDigits_eq_digit_rev b n P (List.length (Nat.toDigits b n) - 1 - i)]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.getD (toDigits b n) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b n)) (List.length (toDigits b n) - 1 - i) (Char.ofNat 48)
Theorem: Nat.toDigits_eq_digit
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.getD (toDigits b n) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b n)) (List.length (toDigits b n) - 1 - i) (Char.ofNat 48)
Tactic:
rw [ List.getD, List.getD, List.get?_reverse]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ Option.getD (List.get? (toDigits b n) i) (Char.ofNat 48) =
    Option.getD (List.get? (toDigits b n) (List.length (toDigits b n) - 1 - (List.length (toDigits b n) - 1 - i)))
      (Char.ofNat 48)

case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)
Theorem: Nat.toDigits_eq_digit
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ Option.getD (List.get? (toDigits b n) i) (Char.ofNat 48) =
    Option.getD (List.get? (toDigits b n) (List.length (toDigits b n) - 1 - (List.length (toDigits b n) - 1 - i)))
      (Char.ofNat 48)

case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)
Tactic:
congr
Proof state after:
case e_a.e_a
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ i = List.length (toDigits b n) - 1 - (List.length (toDigits b n) - 1 - i)

case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)
Theorem: Nat.toDigits_eq_digit
Proof state before:
case e_a.e_a
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ i = List.length (toDigits b n) - 1 - (List.length (toDigits b n) - 1 - i)

case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)
Tactic:
. have h₂: List.length (toDigits b n) - 1 ≥ (List.length (toDigits b n) - 1 - i) := by simp
  have h₃: List.length (toDigits b n) ≥ 1 := by calc 
    List.length (toDigits b n) > i := h
    _ ≥ 0 := by simp only [ge_iff_le, _root_.zero_le]
  have h₄: i ≤ List.length (toDigits b n) - 1 := by apply Nat.le_pred_of_lt; exact h
  zify [h₂, h₃, h₄]
  apply Int.eq_of_sub_eq_zero
  ring_nf
Proof state after:
case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)
Theorem: Nat.toDigits_eq_digit
Proof state before:
case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)
Tactic:
. rw [Nat.sub_sub]
  apply Nat.sub_lt_self
  . simp only [add_pos_iff, true_or]
  . rw [Nat.add_comm]
    apply Nat.lt_iff_add_one_le.1 h
Proof state after:
no goals
Theorem: Nat.toDigits_eq_digit
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.toDigits_eq_digit
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
h₂ : List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
⊢ List.length (toDigits b n) ≥ 1
Tactic:
calc 
List.length (toDigits b n) > i := h
_ ≥ 0 := by simp only [ge_iff_le, _root_.zero_le]
Proof state after:
no goals
Theorem: Nat.toDigits_eq_digit
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
h₂ : List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
⊢ i ≥ 0
Tactic:
simp only [ge_iff_le, _root_.zero_le]
Proof state after:
no goals
Theorem: Nat.toDigits_eq_digit
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
h₂ : List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
h₃ : List.length (toDigits b n) ≥ 1
⊢ i ≤ List.length (toDigits b n) - 1
Tactic:
apply Nat.le_pred_of_lt
Proof state after:
case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
h₂ : List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
h₃ : List.length (toDigits b n) ≥ 1
⊢ i < List.length (toDigits b n)
Theorem: Nat.toDigits_eq_digit
Proof state before:
case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
h₂ : List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
h₃ : List.length (toDigits b n) ≥ 1
⊢ i < List.length (toDigits b n)
Tactic:
exact h
Proof state after:
no goals