[GOAL]
n m : ℕ
⊢ succ n * m = 0 → succ n = 0 ∨ m = 0
[PROOFSTEP]
rw [succ_mul]
[GOAL]
n m : ℕ
⊢ n * m + m = 0 → succ n = 0 ∨ m = 0
[PROOFSTEP]
intro h
[GOAL]
n m : ℕ
h : n * m + m = 0
⊢ succ n = 0 ∨ m = 0
[PROOFSTEP]
exact Or.inr (Nat.eq_zero_of_add_eq_zero_left h)
[GOAL]
m : ℕ
h : bit0 0 = bit0 (m + 1)
⊢ 0 = m + 1
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
h : bit0 (n + 1) = bit0 0
⊢ n + 1 = 0
[PROOFSTEP]
contradiction
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
⊢ n + 1 = m + 1
[PROOFSTEP]
have : succ (succ (n + n)) = succ (succ (m + m)) :=
  by
  unfold bit0 at h ; simp [add_one, add_succ, succ_add] at h 
  have aux : n + n = m + m := h; rw [aux]
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
⊢ succ (succ (n + n)) = succ (succ (m + m))
[PROOFSTEP]
unfold bit0 at h 
[GOAL]
n m : ℕ
h : n + 1 + (n + 1) = m + 1 + (m + 1)
⊢ succ (succ (n + n)) = succ (succ (m + m))
[PROOFSTEP]
simp [add_one, add_succ, succ_add] at h 
[GOAL]
n m : ℕ
h : n + n = m + m
⊢ succ (succ (n + n)) = succ (succ (m + m))
[PROOFSTEP]
have aux : n + n = m + m := h
[GOAL]
n m : ℕ
h aux : n + n = m + m
⊢ succ (succ (n + n)) = succ (succ (m + m))
[PROOFSTEP]
rw [aux]
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this : succ (succ (n + n)) = succ (succ (m + m))
⊢ n + 1 = m + 1
[PROOFSTEP]
have : n + n = m + m := by repeat injection this with this
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this : succ (succ (n + n)) = succ (succ (m + m))
⊢ n + n = m + m
[PROOFSTEP]
repeat injection this with this
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this : succ (succ (n + n)) = succ (succ (m + m))
⊢ n + n = m + m
[PROOFSTEP]
injection this with this
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this : succ (n + n) = succ (m + m)
⊢ n + n = m + m
[PROOFSTEP]
injection this with this
[GOAL]

[PROOFSTEP]
injection this with this
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this✝ : succ (succ (n + n)) = succ (succ (m + m))
this : n + n = m + m
⊢ n + 1 = m + 1
[PROOFSTEP]
have : n = m := Nat.bit0_inj this
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this✝¹ : succ (succ (n + n)) = succ (succ (m + m))
this✝ : n + n = m + m
this : n = m
⊢ n + 1 = m + 1
[PROOFSTEP]
rw [this]
[GOAL]
n m : ℕ
h : bit1 n = bit1 m
⊢ succ (bit0 n) = succ (bit0 m)
[PROOFSTEP]
simp [Nat.bit1_eq_succ_bit0] at h 
[GOAL]
n m : ℕ
h : bit0 n = bit0 m
⊢ succ (bit0 n) = succ (bit0 m)
[PROOFSTEP]
rw [h]
[GOAL]
n m : ℕ
h : bit1 n = bit1 m
this : succ (bit0 n) = succ (bit0 m)
⊢ bit0 n = bit0 m
[PROOFSTEP]
injection this
[GOAL]
h : 0 ≠ 0
⊢ 1 < bit1 0
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
_h : succ n ≠ 0
⊢ 1 < bit1 (succ n)
[PROOFSTEP]
rw [Nat.bit1_succ_eq]
[GOAL]
n : ℕ
_h : succ n ≠ 0
⊢ 1 < succ (succ (bit1 n))
[PROOFSTEP]
apply succ_lt_succ
[GOAL]
case a
n : ℕ
_h : succ n ≠ 0
⊢ 0 < bit1 n + 1
[PROOFSTEP]
apply zero_lt_succ
[GOAL]
h : 0 ≠ 0
⊢ 1 < bit0 0
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
_h : succ n ≠ 0
⊢ 1 < bit0 (succ n)
[PROOFSTEP]
rw [Nat.bit0_succ_eq]
[GOAL]
n : ℕ
_h : succ n ≠ 0
⊢ 1 < succ (succ (bit0 n))
[PROOFSTEP]
apply succ_lt_succ
[GOAL]
case a
n : ℕ
_h : succ n ≠ 0
⊢ 0 < bit0 n + 1
[PROOFSTEP]
apply zero_lt_succ
[GOAL]
n m : ℕ
h : n < succ m
this✝ : n ≤ m
this : succ (n + n) ≤ succ (m + m)
⊢ succ (n + n) ≤ succ m + m
[PROOFSTEP]
rw [succ_add]
[GOAL]
n m : ℕ
h : n < succ m
this✝ : n ≤ m
this : succ (n + n) ≤ succ (m + m)
⊢ succ (n + n) ≤ succ (m + m)
[PROOFSTEP]
assumption
[GOAL]
B : Sort u
n : ℕ
H1 : n = 0 → B
H2 : (m : ℕ) → n = succ m → B
⊢ B
[PROOFSTEP]
induction' h : n
[GOAL]
case zero
B : Sort u
n : ℕ
H1 : n = 0 → B
H2 : (m : ℕ) → n = succ m → B
x✝ : ℕ
h✝ : n = x✝
h : n = zero
⊢ B
[PROOFSTEP]
exact H1 h
[GOAL]
case succ
B : Sort u
n : ℕ
H1 : n = 0 → B
H2 : (m : ℕ) → n = succ m → B
x✝ : ℕ
h✝ : n = x✝
n✝ : ℕ
n_ih✝ : n = n✝ → B
h : n = succ n✝
⊢ B
[PROOFSTEP]
exact H2 _ h
[GOAL]
x y k : ℕ
h : k ≤ y
⊢ x ≤ y - k ↔ x + k ≤ y
[PROOFSTEP]
rw [← Nat.add_sub_cancel x k, Nat.sub_le_sub_iff_right h, Nat.add_sub_cancel]
[GOAL]
m n k : ℕ
⊢ m - n - k = m - k - n
[PROOFSTEP]
rw [Nat.sub_sub, Nat.sub_sub, Nat.add_comm]
[GOAL]
x : ℕ
d : Decidable (x % 2 = 1)
⊢ (bif decide (x % 2 = 1) then 1 else 0) = x % 2
[PROOFSTEP]
by_cases h : x % 2 = 1
[GOAL]
case pos
x : ℕ
d : Decidable (x % 2 = 1)
h : x % 2 = 1
⊢ (bif decide (x % 2 = 1) then 1 else 0) = x % 2
[PROOFSTEP]
simp! [*]
[GOAL]
case neg
x : ℕ
d : Decidable (x % 2 = 1)
h : ¬x % 2 = 1
⊢ (bif decide (x % 2 = 1) then 1 else 0) = x % 2
[PROOFSTEP]
cases mod_two_eq_zero_or_one x
[GOAL]
case neg.inl
x : ℕ
d : Decidable (x % 2 = 1)
h : ¬x % 2 = 1
h✝ : x % 2 = 0
⊢ (bif decide (x % 2 = 1) then 1 else 0) = x % 2
[PROOFSTEP]
simp! [*, Nat.zero_ne_one]
[GOAL]
case neg.inr
x : ℕ
d : Decidable (x % 2 = 1)
h : ¬x % 2 = 1
h✝ : x % 2 = 1
⊢ (bif decide (x % 2 = 1) then 1 else 0) = x % 2
[PROOFSTEP]
simp! [*, Nat.zero_ne_one]
[GOAL]
m n k : ℕ
H : 0 < m
⊢ m * n / (m * k) = n / k
[PROOFSTEP]
rw [← Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n : ℕ
pn : p n
m✝ m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc Nat.lbp k
k : ℕ
kn : n ≤ k + succ m
y : ℕ
r : Nat.lbp y k
_a : ∀ (k_1 : ℕ), k_1 ≤ k → ¬p k_1
⊢ n ≤ k + 1 + m
[PROOFSTEP]
rw [Nat.add_right_comm]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n : ℕ
pn : p n
m✝ m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc Nat.lbp k
k : ℕ
kn : n ≤ k + succ m
y : ℕ
r : Nat.lbp y k
_a : ∀ (k_1 : ℕ), k_1 ≤ k → ¬p k_1
⊢ n ≤ k + m + 1
[PROOFSTEP]
exact kn
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
m : ℕ
IH : (y : ℕ) → Nat.lbp y m → (fun k => (∀ (n : ℕ), n < k → ¬p n) → { n // p n ∧ ∀ (m : ℕ), m < n → ¬p m }) y
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
⊢ ¬p n
[PROOFSTEP]
rw [e]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
m : ℕ
IH : (y : ℕ) → Nat.lbp y m → (fun k => (∀ (n : ℕ), n < k → ¬p n) → { n // p n ∧ ∀ (m : ℕ), m < n → ¬p m }) y
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
⊢ ¬p m
[PROOFSTEP]
exact pm
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
[PROOFSTEP]
induction f with (simp only [Nat.toDigitsCore, List.length]; intro n l1 l2 hlen)
| zero => assumption
| succ f ih =>
  by_cases hx : n / b = 0
  case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
  case neg =>
    simp only [hx, if_false]
    specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
    simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih 
    exact ih trivial
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
[PROOFSTEP]
induction f with (simp only [Nat.toDigitsCore, List.length]; intro n l1 l2 hlen)
| zero => assumption
| succ f ih =>
  by_cases hx : n / b = 0
  case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
  case neg =>
    simp only [hx, if_false]
    specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
    simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih 
    exact ih trivial
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b zero n l1) = List.length (toDigitsCore b zero n l2)
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length]
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
⊢ ℕ → ∀ (l1 l2 : List Char), List.length l1 = List.length l2 → List.length l1 = List.length l2
[PROOFSTEP]
intro n l1 l2 hlen
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
⊢ List.length l1 = List.length l2
[PROOFSTEP]

| zero => assumption
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
⊢ List.length l1 = List.length l2
[PROOFSTEP]
assumption
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 →
      List.length (toDigitsCore b (succ f) n l1) = List.length (toDigitsCore b (succ f) n l2)
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 →
      List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
        List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
intro n l1 l2 hlen
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]

| succ f ih =>
  by_cases hx : n / b = 0
  case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
  case neg =>
    simp only [hx, if_false]
    specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
    simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih 
    exact ih trivial
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
by_cases hx : n / b = 0
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
case neg =>
  simp only [hx, if_false]
  specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
  simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih 
  exact ih trivial
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
case neg =>
  simp only [hx, if_false]
  specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
  simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih 
  exact ih trivial
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
simp only [hx, if_false]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
⊢ List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
ih :
  List.length (digitChar (n % b) :: l1) = List.length (digitChar (n % b) :: l2) →
    List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
      List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
⊢ List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih 
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
ih :
  True →
    List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
      List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
⊢ List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
exact ih trivial
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
[PROOFSTEP]
induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
| succ f ih =>
  by_cases hnb : (n / b) = 0
  case pos => simp only [hnb, if_true, List.length]
  case neg =>
    generalize hx : Nat.digitChar (n % b) = x
    simp only [hx, hnb, if_false] at ih 
    simp only [hnb, if_false]
    specialize ih (n / b) c (x :: tl)
    rw [← ih]
    have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
    apply to_digits_core_lens_eq_aux
    exact lens_eq
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
[PROOFSTEP]
induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
| succ f ih =>
  by_cases hnb : (n / b) = 0
  case pos => simp only [hnb, if_true, List.length]
  case neg =>
    generalize hx : Nat.digitChar (n % b) = x
    simp only [hx, hnb, if_false] at ih 
    simp only [hnb, if_false]
    specialize ih (n / b) c (x :: tl)
    rw [← ih]
    have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
    apply to_digits_core_lens_eq_aux
    exact lens_eq
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b (succ f) n (c :: tl)) = List.length (toDigitsCore b (succ f) n tl) + 1
[PROOFSTEP]
intro n c tl
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
⊢ List.length (toDigitsCore b (succ f) n (c :: tl)) = List.length (toDigitsCore b (succ f) n tl) + 1
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]

| succ f ih =>
  by_cases hnb : (n / b) = 0
  case pos => simp only [hnb, if_true, List.length]
  case neg =>
    generalize hx : Nat.digitChar (n % b) = x
    simp only [hx, hnb, if_false] at ih 
    simp only [hnb, if_false]
    specialize ih (n / b) c (x :: tl)
    rw [← ih]
    have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
    apply to_digits_core_lens_eq_aux
    exact lens_eq
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
by_cases hnb : (n / b) = 0
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
case pos => simp only [hnb, if_true, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
case pos => simp only [hnb, if_true, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
simp only [hnb, if_true, List.length]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
case neg =>
  generalize hx : Nat.digitChar (n % b) = x
  simp only [hx, hnb, if_false] at ih 
  simp only [hnb, if_false]
  specialize ih (n / b) c (x :: tl)
  rw [← ih]
  have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
  apply to_digits_core_lens_eq_aux
  exact lens_eq
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
case neg =>
  generalize hx : Nat.digitChar (n % b) = x
  simp only [hx, hnb, if_false] at ih 
  simp only [hnb, if_false]
  specialize ih (n / b) c (x :: tl)
  rw [← ih]
  have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
  apply to_digits_core_lens_eq_aux
  exact lens_eq
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
generalize hx : Nat.digitChar (n % b) = x
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
⊢ List.length (if n / b = 0 then x :: c :: tl else toDigitsCore b f (n / b) (x :: c :: tl)) =
    List.length (if n / b = 0 then x :: tl else toDigitsCore b f (n / b) (x :: tl)) + 1
[PROOFSTEP]
simp only [hx, hnb, if_false] at ih 
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
⊢ List.length (if n / b = 0 then x :: c :: tl else toDigitsCore b f (n / b) (x :: c :: tl)) =
    List.length (if n / b = 0 then x :: tl else toDigitsCore b f (n / b) (x :: tl)) + 1
[PROOFSTEP]
simp only [hnb, if_false]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
⊢ List.length (toDigitsCore b f (n / b) (x :: c :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
[PROOFSTEP]
specialize ih (n / b) c (x :: tl)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
ih : List.length (toDigitsCore b f (n / b) (c :: x :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
⊢ List.length (toDigitsCore b f (n / b) (x :: c :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
[PROOFSTEP]
rw [← ih]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
ih : List.length (toDigitsCore b f (n / b) (c :: x :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
⊢ List.length (toDigitsCore b f (n / b) (x :: c :: tl)) = List.length (toDigitsCore b f (n / b) (c :: x :: tl))
[PROOFSTEP]
have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
ih : List.length (toDigitsCore b f (n / b) (c :: x :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
⊢ List.length (x :: c :: tl) = List.length (c :: x :: tl)
[PROOFSTEP]
simp
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
ih : List.length (toDigitsCore b f (n / b) (c :: x :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
lens_eq : List.length (x :: c :: tl) = List.length (c :: x :: tl)
⊢ List.length (toDigitsCore b f (n / b) (x :: c :: tl)) = List.length (toDigitsCore b f (n / b) (c :: x :: tl))
[PROOFSTEP]
apply to_digits_core_lens_eq_aux
[GOAL]
case a
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
ih : List.length (toDigitsCore b f (n / b) (c :: x :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
lens_eq : List.length (x :: c :: tl) = List.length (c :: x :: tl)
⊢ List.length (x :: c :: tl) = List.length (c :: x :: tl)
[PROOFSTEP]
exact lens_eq
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b zero n (c :: tl)) = List.length (toDigitsCore b zero n tl) + 1
[PROOFSTEP]
intro n c tl
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b n : ℕ
c : Char
tl : List Char
⊢ List.length (toDigitsCore b zero n (c :: tl)) = List.length (toDigitsCore b zero n tl) + 1
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ succ e → n / b < b ^ e
[PROOFSTEP]
simp only [Nat.pow_succ]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e * b → n / b < b ^ e
[PROOFSTEP]
exact (@Nat.div_lt_iff_lt_mul b n (b ^ e) h_b_pos).mpr
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (toDigitsCore b f n []) ≤ e
[PROOFSTEP]
induction f generalizing n e hlt h_e_pos with simp only [Nat.toDigitsCore, List.length, Nat.zero_le]
| succ f ih =>
  cases e with
  | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
  | succ e =>
    by_cases h_pred_pos : 0 < e
    case pos =>
      have _ : 0 < b := Nat.lt_trans (by decide) h
      specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
      by_cases hdiv_ten : n / b = 0
      case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
      case neg =>
        simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
        exact Nat.succ_le_succ ih
    case neg =>
      have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
      rw [‹e = 0›]
      have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
      have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
      simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (toDigitsCore b f n []) ≤ e
[PROOFSTEP]
induction f generalizing n e hlt h_e_pos with simp only [Nat.toDigitsCore, List.length, Nat.zero_le]
| succ f ih =>
  cases e with
  | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
  | succ e =>
    by_cases h_pred_pos : 0 < e
    case pos =>
      have _ : 0 < b := Nat.lt_trans (by decide) h
      specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
      by_cases hdiv_ten : n / b = 0
      case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
      case neg =>
        simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
        exact Nat.succ_le_succ ih
    case neg =>
      have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
      rw [‹e = 0›]
      have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
      have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
      simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (toDigitsCore b (succ f) n []) ≤ e
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length, Nat.zero_le]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ e
[PROOFSTEP]

| succ f ih =>
  cases e with
  | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
  | succ e =>
    by_cases h_pred_pos : 0 < e
    case pos =>
      have _ : 0 < b := Nat.lt_trans (by decide) h
      specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
      by_cases hdiv_ten : n / b = 0
      case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
      case neg =>
        simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
        exact Nat.succ_le_succ ih
    case neg =>
      have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
      rw [‹e = 0›]
      have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
      have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
      simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ e
[PROOFSTEP]
cases e with
| zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
| succ e =>
  by_cases h_pred_pos : 0 < e
  case pos =>
    have _ : 0 < b := Nat.lt_trans (by decide) h
    specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
    by_cases hdiv_ten : n / b = 0
    case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
    case neg =>
      simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
      exact Nat.succ_le_succ ih
  case neg =>
    have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
    rw [‹e = 0›]
    have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
    have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
    simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ e
[PROOFSTEP]
cases e with
| zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
| succ e =>
  by_cases h_pred_pos : 0 < e
  case pos =>
    have _ : 0 < b := Nat.lt_trans (by decide) h
    specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
    by_cases hdiv_ten : n / b = 0
    case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
    case neg =>
      simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
      exact Nat.succ_le_succ ih
  case neg =>
    have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
    rw [‹e = 0›]
    have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
    have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
    simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case succ.zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n : ℕ
hlt : n < b ^ zero
h_e_pos : 0 < zero
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ zero
[PROOFSTEP]

| zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
[GOAL]
case succ.zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n : ℕ
hlt : n < b ^ zero
h_e_pos : 0 < zero
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ zero
[PROOFSTEP]
exact False.elim (Nat.lt_irrefl 0 h_e_pos)
[GOAL]
case succ.succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]

| succ e =>
  by_cases h_pred_pos : 0 < e
  case pos =>
    have _ : 0 < b := Nat.lt_trans (by decide) h
    specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
    by_cases hdiv_ten : n / b = 0
    case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
    case neg =>
      simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
      exact Nat.succ_le_succ ih
  case neg =>
    have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
    rw [‹e = 0›]
    have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
    have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
    simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case succ.succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
by_cases h_pred_pos : 0 < e
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case pos =>
  have _ : 0 < b := Nat.lt_trans (by decide) h
  specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
  by_cases hdiv_ten : n / b = 0
  case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
  case neg =>
    simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
    exact Nat.succ_le_succ ih
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case pos =>
  have _ : 0 < b := Nat.lt_trans (by decide) h
  specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
  by_cases hdiv_ten : n / b = 0
  case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
  case neg =>
    simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
    exact Nat.succ_le_succ ih
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
have _ : 0 < b := Nat.lt_trans (by decide) h
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
⊢ 0 < 1
[PROOFSTEP]
decide
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
by_cases hdiv_ten : n / b = 0
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : ¬n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
simp only [hdiv_ten]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : n / b = 0
⊢ List.length (if True then [digitChar (n % b)] else toDigitsCore b f 0 [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
exact Nat.le.step h_pred_pos
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : ¬n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case neg =>
  simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
  exact Nat.succ_le_succ ih
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : ¬n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case neg =>
  simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
  exact Nat.succ_le_succ ih
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : ¬n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : ¬n / b = 0
⊢ List.length (toDigitsCore b f (n / b) []) + 1 ≤ succ e
[PROOFSTEP]
exact Nat.succ_le_succ ih
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case neg =>
  have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
  rw [‹e = 0›]
  have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
  have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
  simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case neg =>
  have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
  rw [‹e = 0›]
  have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
  have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
  simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
x✝ : e = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
rw [‹e = 0›]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
x✝ : e = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ 0
[PROOFSTEP]
have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
x✝ : e = 0
⊢ b ^ 1 = b
[PROOFSTEP]
simp only [pow_succ, pow_zero, Nat.one_mul]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
x✝¹ : e = 0
x✝ : b ^ 1 = b
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ 0
[PROOFSTEP]
have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
x✝² : e = 0
x✝¹ : b ^ 1 = b
x✝ : n < b
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ 0
[PROOFSTEP]
simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (toDigitsCore b zero n []) ≤ e
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length, Nat.zero_le]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n e : ℕ
⊢ 0 < e → n < 10 ^ e → String.length (Nat.repr n) ≤ e
[PROOFSTEP]
cases n with (intro e0 he; simp only [Nat.repr, Nat.toDigits, String.length, List.asString])
| zero => assumption
| succ n =>
  by_cases hterm : n.succ / 10 = 0
  case pos => simp only [hterm, Nat.toDigitsCore]; assumption
  case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n e : ℕ
⊢ 0 < e → n < 10 ^ e → String.length (Nat.repr n) ≤ e
[PROOFSTEP]
cases n with (intro e0 he; simp only [Nat.repr, Nat.toDigits, String.length, List.asString])
| zero => assumption
| succ n =>
  by_cases hterm : n.succ / 10 = 0
  case pos => simp only [hterm, Nat.toDigitsCore]; assumption
  case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e : ℕ
⊢ 0 < e → zero < 10 ^ e → String.length (Nat.repr zero) ≤ e
[PROOFSTEP]
intro e0 he
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e : ℕ
e0 : 0 < e
he : zero < 10 ^ e
⊢ String.length (Nat.repr zero) ≤ e
[PROOFSTEP]
simp only [Nat.repr, Nat.toDigits, String.length, List.asString]
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e : ℕ
e0 : 0 < e
he : zero < 10 ^ e
⊢ List.length (toDigitsCore 10 (zero + 1) zero []) ≤ e
[PROOFSTEP]

| zero => assumption
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e : ℕ
e0 : 0 < e
he : zero < 10 ^ e
⊢ List.length (toDigitsCore 10 (zero + 1) zero []) ≤ e
[PROOFSTEP]
assumption
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
⊢ 0 < e → succ n < 10 ^ e → String.length (Nat.repr (succ n)) ≤ e
[PROOFSTEP]
intro e0 he
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
⊢ String.length (Nat.repr (succ n)) ≤ e
[PROOFSTEP]
simp only [Nat.repr, Nat.toDigits, String.length, List.asString]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]

| succ n =>
  by_cases hterm : n.succ / 10 = 0
  case pos => simp only [hterm, Nat.toDigitsCore]; assumption
  case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
by_cases hterm : n.succ / 10 = 0
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : ¬succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
case pos => simp only [hterm, Nat.toDigitsCore]; assumption
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
case pos => simp only [hterm, Nat.toDigitsCore]; assumption
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
simp only [hterm, Nat.toDigitsCore]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : succ n / 10 = 0
⊢ List.length
      (if True then [digitChar (succ n % 10)]
      else
        if True then [digitChar (0 % 10), digitChar (succ n % 10)]
        else toDigitsCore 10 n (0 / 10) [digitChar (0 % 10), digitChar (succ n % 10)]) ≤
    e
[PROOFSTEP]
assumption
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : ¬succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : ¬succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : ¬succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : ¬succ n / 10 = 0
⊢ 2 ≤ 10
[PROOFSTEP]
decide
