Theorem: Nat.toDigitsCore_length_eq_log (One.lean)

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]
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

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]
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)

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]
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

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
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

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
State after:
no goals

State before:
accum : List Char
b fuel n : ℕ
P : b > 1
R : fuel > n
⊢ accum = [] ++ accum
Tactic:
simp only [List.nil_append]
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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
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

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)
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

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
State after:
no goals

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
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

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
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

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]
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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]
State after:
no goals

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]
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

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]
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

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
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

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]
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

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
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

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
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

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 []
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
⊢ [] = [] ++ []

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
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
⊢ [] = [] ++ []

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals