-- Mathlib/Data/Nat/Digits.lean
/-- The String representation produced by toDigitsCore has the proper length relative to
the number of digits in `n < e` for some base `b`. Since this works with any base greater
than one, it can be used for binary, decimal, and hex. -/
lemma toDigitsCore_length (b : Nat) (h : 2 <= b) (f n e : Nat)
    (hlt : n < b ^ e) (h_e_pos : 0 < e) : (Nat.toDigitsCore b f n []).length <= e

Proof state:
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
x✝ : 0 < b
ih : (b.toDigitsCore f (n / b) []).length ≤ e
hdiv_ten : ¬n / b = 0
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Tactic:
simp only [hdiv_ten,
  toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b), if_false]

Result:
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
x✝ : 0 < b
ih : (b.toDigitsCore f (n / b) []).length ≤ e
hdiv_ten : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) []).length + 1 ≤ e + 1

Proof state:
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
x✝ : 0 < b
ih : (b.toDigitsCore f (n / b) []).length ≤ e
hdiv_ten : n / b = 0
⊢ (if True then [(n % b).digitChar] else b.toDigitsCore f 0 [(n % b).digitChar]).length ≤ e + 1

Tactic:
exact Nat.le.step h_pred_pos

Result:
no goals

Proof state:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
hlt : n < b ^ (0 + 1)
h_e_pos : 0 < 0 + 1
h_pred_pos : ¬0 < 0
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1

Tactic:
have _ : b ^ 1 = b := by simp only [Nat.pow_succ, pow_zero, Nat.one_mul]

Result:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
hlt : n < b ^ (0 + 1)
h_e_pos : 0 < 0 + 1
h_pred_pos : ¬0 < 0
x✝ : b ^ 1 = b
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1

Proof state:
case succ
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e

Tactic:
cases e with
| zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
| succ e =>
  if h_pred_pos : 0 < e then
    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
    if hdiv_ten : n / b = 0 then
      simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
    else
      simp only [hdiv_ten,
        toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b), if_false]
      exact Nat.succ_le_succ ih
  else
    obtain rfl : e = 0 := Nat.eq_zero_of_not_pos h_pred_pos
    have _ : b ^ 1 = b := by simp only [Nat.pow_succ, pow_zero, Nat.one_mul]
    have _ : n < b := ‹b ^ 1 = b› ▸ hlt
    simp [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0)]

Result:
no goals

Proof state:
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
x✝ : 0 < b
ih : (b.toDigitsCore f (n / b) []).length ≤ e
hdiv_ten : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) []).length + 1 ≤ e + 1

Tactic:
exact Nat.succ_le_succ ih

Result:
no goals

Proof state:
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
x✝ : 0 < b
ih : (b.toDigitsCore f (n / b) []).length ≤ e
hdiv_ten : n / b = 0
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Tactic:
simp only [hdiv_ten]

Result:
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
x✝ : 0 < b
ih : (b.toDigitsCore f (n / b) []).length ≤ e
hdiv_ten : n / b = 0
⊢ (if True then [(n % b).digitChar] else b.toDigitsCore f 0 [(n % b).digitChar]).length ≤ e + 1

Proof state:
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ (b.toDigitsCore f n []).length ≤ e

Tactic:
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 =>
    if h_pred_pos : 0 < e then
      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
      if hdiv_ten : n / b = 0 then
        simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
      else
        simp only [hdiv_ten,
          toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b), if_false]
        exact Nat.succ_le_succ ih
    else
      obtain rfl : e = 0 := Nat.eq_zero_of_not_pos h_pred_pos
      have _ : b ^ 1 = b := by simp only [Nat.pow_succ, pow_zero, Nat.one_mul]
      have _ : n < b := ‹b ^ 1 = b› ▸ hlt
      simp [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0)]

Result:
no goals

Proof state:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Tactic:
have _ : 0 < b := Nat.lt_trans (by decide) h

Result:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
x✝ : 0 < b
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Proof state:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
case succ.succ
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Tactic:
if h_pred_pos : 0 < e then
  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
  if hdiv_ten : n / b = 0 then
    simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
  else
    simp only [hdiv_ten,
      toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b), if_false]
    exact Nat.succ_le_succ ih
else
  obtain rfl : e = 0 := Nat.eq_zero_of_not_pos h_pred_pos
  have _ : b ^ 1 = b := by simp only [Nat.pow_succ, pow_zero, Nat.one_mul]
  have _ : n < b := ‹b ^ 1 = b› ▸ hlt
  simp [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0)]

Result:
no goals

Proof state:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
hlt : n < b ^ (0 + 1)
h_e_pos : 0 < 0 + 1
h_pred_pos : ¬0 < 0
⊢ b ^ 1 = b

Tactic:
simp only [Nat.pow_succ, pow_zero, Nat.one_mul]

Result:
no goals

Proof state:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
x✝ : 0 < b
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Tactic:
specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos

Result:
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
x✝ : 0 < b
ih : (b.toDigitsCore f (n / b) []).length ≤ e
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1