-- Mathlib/Data/Nat/Digits.lean
lemma toDigitsCore_lens_eq (b f : Nat) : ∀ (n : Nat) (c : Char) (tl : List Char),
    (Nat.toDigitsCore b f n (c :: tl)).length = (Nat.toDigitsCore b f n tl).length + 1

Proof state:
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
ih : (b.toDigitsCore f (n / b) (c :: x :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1
lens_eq : (x :: c :: tl).length = (c :: x :: tl).length
⊢ (b.toDigitsCore f (n / b) (x :: c :: tl)).length = (b.toDigitsCore f (n / b) (c :: x :: tl)).length

Tactic:
apply toDigitsCore_lens_eq_aux

Result:
case a
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
ih : (b.toDigitsCore f (n / b) (c :: x :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1
lens_eq : (x :: c :: tl).length = (c :: x :: tl).length
⊢ (x :: c :: tl).length = (c :: x :: tl).length

Proof state:
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
⊢ (if n / b = 0 then x :: c :: tl else b.toDigitsCore f (n / b) (x :: c :: tl)).length =
    (if n / b = 0 then x :: tl else b.toDigitsCore f (n / b) (x :: tl)).length + 1

Tactic:
simp only [hnb, if_false]

Result:
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
⊢ (b.toDigitsCore f (n / b) (x :: c :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1

Proof state:
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
ih : (b.toDigitsCore f (n / b) (c :: x :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1
⊢ (b.toDigitsCore f (n / b) (x :: c :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1

Tactic:
rw [← ih]

Result:
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
ih : (b.toDigitsCore f (n / b) (c :: x :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1
⊢ (b.toDigitsCore f (n / b) (x :: c :: tl)).length = (b.toDigitsCore f (n / b) (c :: x :: tl)).length

Proof state:
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
⊢ (b.toDigitsCore f (n / b) (x :: c :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1

Tactic:
specialize ih (n / b) c (x :: tl)

Result:
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
ih : (b.toDigitsCore f (n / b) (c :: x :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1
⊢ (b.toDigitsCore f (n / b) (x :: c :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1

Proof state:
case a
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
ih : (b.toDigitsCore f (n / b) (c :: x :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1
lens_eq : (x :: c :: tl).length = (c :: x :: tl).length
⊢ (x :: c :: tl).length = (c :: x :: tl).length

Tactic:
exact lens_eq

Result:
no goals

Proof state:
case zero
b n : ℕ
c : Char
tl : List Char
⊢ (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1

Tactic:
simp only [Nat.toDigitsCore, List.length]

Result:
no goals

Proof state:
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
⊢ (if n / b = 0 then (n % b).digitChar :: c :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: c :: tl)).length =
    (if n / b = 0 then (n % b).digitChar :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: tl)).length + 1

Tactic:
generalize hx : Nat.digitChar (n % b) = x

Result:
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
⊢ (if n / b = 0 then x :: c :: tl else b.toDigitsCore f (n / b) (x :: c :: tl)).length =
    (if n / b = 0 then x :: tl else b.toDigitsCore f (n / b) (x :: tl)).length + 1

Proof state:
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
hnb : n / b = 0
⊢ (if n / b = 0 then (n % b).digitChar :: c :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: c :: tl)).length =
    (if n / b = 0 then (n % b).digitChar :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: tl)).length + 1

Tactic:
simp only [hnb, if_true, List.length]

Result:
no goals

Proof state:
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
ih : (b.toDigitsCore f (n / b) (c :: x :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1
⊢ (x :: c :: tl).length = (c :: x :: tl).length

Tactic:
simp

Result:
no goals

Proof state:
case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
⊢ (if n / b = 0 then (n % b).digitChar :: c :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: c :: tl)).length =
    (if n / b = 0 then (n % b).digitChar :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: tl)).length + 1

Tactic:
if hnb : (n / b) = 0 then
  simp only [hnb, if_true, List.length]
else
  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 toDigitsCore_lens_eq_aux
  exact lens_eq

Result:
no goals

Proof state:
case zero
b : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1

Tactic:
intro n c tl

Result:
case zero
b n : ℕ
c : Char
tl : List Char
⊢ (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1

Proof state:
b f : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1

Tactic:
induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
| succ f ih =>
  if hnb : (n / b) = 0 then
    simp only [hnb, if_true, List.length]
  else
    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 toDigitsCore_lens_eq_aux
    exact lens_eq

Result:
no goals

Proof state:
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
ih : (b.toDigitsCore f (n / b) (c :: x :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1
⊢ (b.toDigitsCore f (n / b) (x :: c :: tl)).length = (b.toDigitsCore f (n / b) (c :: x :: tl)).length

Tactic:
have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp

Result:
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : (n % b).digitChar = x
ih : (b.toDigitsCore f (n / b) (c :: x :: tl)).length = (b.toDigitsCore f (n / b) (x :: tl)).length + 1
lens_eq : (x :: c :: tl).length = (c :: x :: tl).length
⊢ (b.toDigitsCore f (n / b) (x :: c :: tl)).length = (b.toDigitsCore f (n / b) (c :: x :: tl)).length