internlm/Lean-Github huggingface dataset:
Theorem: Nat.toDigitsCore_shift
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) p (Char.ofNat 48)
Tactic:
have heq: i = p + 1 := by cases i with | zero => contradiction | succ n => simp at h; rw [h]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
heq : i = p + 1
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) p (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
heq : i = p + 1
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) p (Char.ofNat 48)
Tactic:
rw [heq]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
heq : i = p + 1
⊢ List.getD (List.reverse (toDigits b n)) (p + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) p (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
heq : i = p + 1
⊢ List.getD (List.reverse (toDigits b n)) (p + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) p (Char.ofNat 48)
Tactic:
apply Nat.toDigitsCore_shift'
Proof state after:
case P
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
heq : i = p + 1
⊢ b > 1
Theorem: Nat.toDigitsCore_shift
Proof state before:
case P
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
heq : i = p + 1
⊢ b > 1
Tactic:
exact P
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
⊢ i = p + 1
Tactic:
cases i with | zero => contradiction | succ n => simp at h; rw [h]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift
Proof state before:
case zero
b n : ℕ
P : b > 1
p : ℕ
igt : zero > 0
h : zero - 1 = p
⊢ zero = p + 1
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift
Proof state before:
case succ
b n✝ : ℕ
P : b > 1
p n : ℕ
igt : succ n > 0
h : succ n - 1 = p
⊢ succ n = p + 1
Tactic:
simp at h
Proof state after:
case succ
b n✝ : ℕ
P : b > 1
p n : ℕ
igt : succ n > 0
h : n = p
⊢ succ n = p + 1
Theorem: Nat.toDigitsCore_shift
Proof state before:
case succ
b n✝ : ℕ
P : b > 1
p n : ℕ
igt : succ n > 0
h : n = p
⊢ succ n = p + 1
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift_full
Proof state before:
b n : ℕ
P : b > 1
⊢ ∀ (i : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
Tactic:
intro i
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift_full
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
Tactic:
induction i generalizing n with
| zero =>
  simp only [zero_eq, pow_zero, Nat.div_one]
| succ i ih =>
  rw [Nat.toDigitsCore_shift]
  . simp
    rw [ih]
    congr 3
    rw [Nat.div_div_eq_div_mul]
    congr 1
    rw [Nat.pow_succ']
  . exact P
  . simp
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift_full
Proof state before:
case zero
b : ℕ
P : b > 1
n : ℕ
⊢ List.getD (List.reverse (toDigits b n)) zero (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ zero))) 0 (Char.ofNat 48)
Tactic:
simp only [zero_eq, pow_zero, Nat.div_one]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift_full
Proof state before:
case succ
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ List.getD (List.reverse (toDigits b n)) (succ i) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ succ i))) 0 (Char.ofNat 48)
Tactic:
rw [Nat.toDigitsCore_shift]
Proof state after:
case succ
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ List.getD (List.reverse (toDigits b (n / b))) (succ i - 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ succ i))) 0 (Char.ofNat 48)

case succ.P
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ b > 1

case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0
Theorem: Nat.toDigitsCore_shift_full
Proof state before:
case succ
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ List.getD (List.reverse (toDigits b (n / b))) (succ i - 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ succ i))) 0 (Char.ofNat 48)

case succ.P
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ b > 1

case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0
Tactic:
. simp
  rw [ih]
  congr 3
  rw [Nat.div_div_eq_div_mul]
  congr 1
  rw [Nat.pow_succ']
Proof state after:
case succ.P
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ b > 1

case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0
Theorem: Nat.toDigitsCore_shift_full
Proof state before:
case succ.P
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ b > 1

case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0
Tactic:
. exact P
Proof state after:
case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0
Theorem: Nat.toDigitsCore_shift_full
Proof state before:
case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0
Tactic:
. simp
Proof state after:
no goals
Theorem: Nat.digit_lt_base
Proof state before:
base n index : ℕ
P : base > 0
⊢ digit base n index < base
Tactic:
unfold Nat.digit
Proof state after:
base n index : ℕ
P : base > 0
⊢ n / base ^ index % base < base
Theorem: Nat.digit_lt_base
Proof state before:
base n index : ℕ
P : base > 0
⊢ n / base ^ index % base < base
Tactic:
apply Nat.mod_lt _ P
Proof state after:
no goals
Theorem: Nat.toDigits_eq_digit_rev
Proof state before:
b n : ℕ
P : b > 1
⊢ ∀ (i : ℕ), List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) = digitChar (digit b n i)
Tactic:
intro i
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) = digitChar (digit b n i)
Theorem: Nat.toDigits_eq_digit_rev
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) = digitChar (digit b n i)
Tactic:
rw [Nat.toDigitsCore_shift_full]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48) = digitChar (digit b n i)

case P
b n : ℕ
P : b > 1
i : ℕ
⊢ b > 1
Theorem: Nat.toDigits_eq_digit_rev
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48) = digitChar (digit b n i)

case P
b n : ℕ
P : b > 1
i : ℕ
⊢ b > 1
Tactic:
. unfold toDigits toDigitsCore digit
  simp only [add_eq, add_zero]
  split
  . next heq =>
    simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.getD._eq_1, List.get?, Option.getD_some]
  . next heq =>
    rw [Nat.todigitsCore_accumulates_suffix]
    simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append,
List.getD._eq_1, List.get?, Option.getD_some]
Proof state after:
case P
b n : ℕ
P : b > 1
i : ℕ
⊢ b > 1
Theorem: Nat.toDigits_eq_digit_rev
Proof state before:
case P
b n : ℕ
P : b > 1
i : ℕ
⊢ b > 1
Tactic:
. exact P
Proof state after:
no goals
Theorem: Nat.toDigits_eq_digit_rev
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b ^ i / b = 0
⊢ List.getD (List.reverse [digitChar (n / b ^ i % b)]) 0 (Char.ofNat 48) = digitChar (n / b ^ i % b)
Tactic:
simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.getD._eq_1, List.get?, Option.getD_some]
Proof state after:
no goals
Theorem: Nat.toDigits_eq_digit_rev
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b ^ i / b = 0
⊢ List.getD (List.reverse (toDigitsCore b (n / b ^ i) (n / b ^ i / b) [digitChar (n / b ^ i % b)])) 0 (Char.ofNat 48) =
    digitChar (n / b ^ i % b)
Tactic:
rw [Nat.todigitsCore_accumulates_suffix]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b ^ i / b = 0
⊢ List.getD (List.reverse (toDigitsCore b (n / b ^ i) (n / b ^ i / b) [] ++ [digitChar (n / b ^ i % b)])) 0
      (Char.ofNat 48) =
    digitChar (n / b ^ i % b)
Theorem: Nat.toDigits_eq_digit_rev
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b ^ i / b = 0
⊢ List.getD (List.reverse (toDigitsCore b (n / b ^ i) (n / b ^ i / b) [] ++ [digitChar (n / b ^ i % b)])) 0
      (Char.ofNat 48) =
    digitChar (n / b ^ i % b)
Tactic:
simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append,
List.getD._eq_1, List.get?, Option.getD_some]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
accum : List Char
b fuel n : ℕ
P : b > 1
R : fuel > n
⊢ List.length (toDigitsCore b fuel n accum) = log b n + 1 + List.length accum
Tactic:
have heq: accum = [] ++ accum := by  simp only [List.nil_append]
Proof state after:
accum : List Char
b fuel n : ℕ
P : b > 1
R : fuel > n
heq : accum = [] ++ accum
⊢ List.length (toDigitsCore b fuel n accum) = log b n + 1 + List.length accum
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
accum : List Char
b fuel n : ℕ
P : b > 1
R : fuel > n
heq : accum = [] ++ accum
⊢ List.length (toDigitsCore b fuel n accum) = log b n + 1 + List.length accum
Tactic:
rw [heq, Nat.toDigitsCore_accumulates]
Proof state after:
accum : List Char
b fuel n : ℕ
P : b > 1
R : fuel > n
heq : accum = [] ++ accum
⊢ List.length (toDigitsCore b fuel n [] ++ accum) = log b n + 1 + List.length ([] ++ accum)
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
accum : List Char
b fuel n : ℕ
P : b > 1
R : fuel > n
heq : accum = [] ++ accum
⊢ List.length (toDigitsCore b fuel n [] ++ accum) = log b n + 1 + List.length ([] ++ accum)
Tactic:
simp only [List.length_append, List.nil_append, add_left_inj]
Proof state after:
accum : List Char
b fuel n : ℕ
P : b > 1
R : fuel > n
heq : accum = [] ++ accum
⊢ List.length (toDigitsCore b fuel n []) = log b n + 1
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
accum : List Char
b fuel n : ℕ
P : b > 1
R : fuel > n
heq : accum = [] ++ accum
⊢ List.length (toDigitsCore b fuel n []) = log b n + 1
Tactic:
induction n using Nat.strong_induction_on generalizing fuel accum
Proof state after:
case h
b : ℕ
P : b > 1
n✝ : ℕ
a✝ :
  ∀ (m : ℕ),
    m < n✝ →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
accum : List Char
fuel : ℕ
R : fuel > n✝
heq : accum = [] ++ accum
⊢ List.length (toDigitsCore b fuel n✝ []) = log b n✝ + 1
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
b : ℕ
P : b > 1
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
accum : List Char
fuel : ℕ
R : fuel > n
heq : accum = [] ++ accum
⊢ List.length (toDigitsCore b fuel n []) = log b n + 1
Tactic:
case h n ih =>
  unfold toDigitsCore
  split
  . next i _ _ _=> 
    exfalso
    apply Nat.not_lt_of_le (Nat.zero_le i)
    apply R
  . next  w y p l =>
    simp; split
    . next i h₂=>
      simp
      left
      have  h: b > 0 := pos_of_gt P
      apply (Nat.div_lt_one_iff h).1
      simp only [h₂, zero_lt_one]
    . 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:
accum : List Char
b fuel n : ℕ
P : b > 1
R : fuel > n
⊢ accum = [] ++ accum
Tactic:
simp only [List.nil_append]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
b : ℕ
P : b > 1
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
accum : List Char
fuel : ℕ
R : fuel > n
heq : accum = [] ++ accum
⊢ List.length (toDigitsCore b fuel n []) = log b n + 1
Tactic:
unfold toDigitsCore
Proof state after:
b : ℕ
P : b > 1
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
accum : List Char
fuel : ℕ
R : fuel > n
heq : accum = [] ++ accum
⊢ List.length
      (match fuel, n, [] with
      | 0, x, ds => ds
      | succ fuel, n, ds =>
        let d := digitChar (n % b);
        let n' := n / b;
        if n' = 0 then d :: ds else toDigitsCore b fuel n' (d :: ds)) =
    log b n + 1
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
b : ℕ
P : b > 1
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
accum : List Char
fuel : ℕ
R : fuel > n
heq : accum = [] ++ accum
⊢ List.length
      (match fuel, n, [] with
      | 0, x, ds => ds
      | succ fuel, n, ds =>
        let d := digitChar (n % b);
        let n' := n / b;
        if n' = 0 then d :: ds else toDigitsCore b fuel n' (d :: ds)) =
    log b n + 1
Tactic:
split
Proof state after:
case h_1
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ),
    m < x✝³ →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : 0 > x✝³
⊢ List.length [] = log b x✝³ + 1

case h_2
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < x✝³ →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ fuel✝ > x✝³
⊢ List.length
      (let d := digitChar (x✝³ % b);
      let n' := x✝³ / b;
      if n' = 0 then [d] else toDigitsCore b fuel✝ n' [d]) =
    log b x✝³ + 1
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case h_1
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ),
    m < x✝³ →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : 0 > x✝³
⊢ List.length [] = log b x✝³ + 1

case h_2
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < x✝³ →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ fuel✝ > x✝³
⊢ List.length
      (let d := digitChar (x✝³ % b);
      let n' := x✝³ / b;
      if n' = 0 then [d] else toDigitsCore b fuel✝ n' [d]) =
    log b x✝³ + 1
Tactic:
. next i _ _ _=> 
  exfalso
  apply Nat.not_lt_of_le (Nat.zero_le i)
  apply R
Proof state after:
case h_2
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < x✝³ →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ fuel✝ > x✝³
⊢ List.length
      (let d := digitChar (x✝³ % b);
      let n' := x✝³ / b;
      if n' = 0 then [d] else toDigitsCore b fuel✝ n' [d]) =
    log b x✝³ + 1
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case h_2
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < x✝³ →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : succ fuel✝ > x✝³
⊢ List.length
      (let d := digitChar (x✝³ % b);
      let n' := x✝³ / b;
      if n' = 0 then [d] else toDigitsCore b fuel✝ n' [d]) =
    log b x✝³ + 1
Tactic:
. next  w y p l =>
  simp; split
  . next i h₂=>
    simp
    left
    have  h: b > 0 := pos_of_gt P
    apply (Nat.div_lt_one_iff h).1
    simp only [h₂, zero_lt_one]
  . 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 x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : 0 > i
⊢ List.length [] = log b i + 1
Tactic:
exfalso
Proof state after:
case h
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : 0 > i
⊢ False
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case h
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : 0 > i
⊢ False
Tactic:
apply Nat.not_lt_of_le (Nat.zero_le i)
Proof state after:
case h
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : 0 > i
⊢ i < 0
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case h
b : ℕ
P : b > 1
accum : List Char
heq : accum = [] ++ accum
i x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ),
    m < i →
      ∀ {accum : List Char} (fuel : ℕ),
        fuel > m → accum = [] ++ accum → List.length (toDigitsCore b fuel m []) = log b m + 1
R : 0 > i
⊢ i < 0
Tactic:
apply R
Proof state after:
no goals
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
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✝
⊢ List.length
      (let d := digitChar (x✝ % b);
      let n' := x✝ / b;
      if n' = 0 then [d] else toDigitsCore b l n' [d]) =
    log b x✝ + 1
Tactic:
simp
Proof state after:
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✝
⊢ List.length (if x✝ / b = 0 then [digitChar (x✝ % b)] else toDigitsCore b l (x✝ / b) [digitChar (x✝ % b)]) =
    log b x✝ + 1
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
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✝
⊢ List.length (if x✝ / b = 0 then [digitChar (x✝ % b)] else toDigitsCore b l (x✝ / b) [digitChar (x✝ % b)]) =
    log b x✝ + 1
Tactic:
split
Proof state after:
case inl
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 [digitChar (x✝ % b)] = log b x✝ + 1

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
Theorem: Nat.toDigitsCore_length_eq_log
Proof state before:
case inl
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 [digitChar (x✝ % b)] = log b x✝ + 1

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 i h₂=>
  simp
  left
  have  h: b > 0 := pos_of_gt P
  apply (Nat.div_lt_one_iff h).1
  simp only [h₂, zero_lt_one]
Proof state after:
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