Theorem: Nat.toDigitsCore_accumulates (One.lean)

State before:
b f n : ℕ
start rest : List Char
⊢ toDigitsCore b f n (start ++ rest) = toDigitsCore b f n start ++ rest
Tactic:
induction f using Nat.strong_induction_on generalizing start rest n with
| h f ih => 
  unfold  toDigitsCore
  split
  . case h.h_1 => simp
  . case h.h_2 f _ _ _ q =>
    simp
    split
    . case inl =>
      simp
    . case inr =>
      rewrite [← List.cons_append]
      rewrite [ih]
      . rfl
      . simp only [lt_succ_self]
State after:
no goals

State before:
case h
b f : ℕ
ih :
  ∀ (m : ℕ),
    m < f → ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
n : ℕ
start rest : List Char
⊢ toDigitsCore b f n (start ++ rest) = toDigitsCore b f n start ++ rest
Tactic:
unfold  toDigitsCore
State after:
case h
b f : ℕ
ih :
  ∀ (m : ℕ),
    m < f → ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
n : ℕ
start rest : List Char
⊢ (match f, n, start ++ rest 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)) =
    (match f, n, start 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)) ++
      rest

State before:
case h
b f : ℕ
ih :
  ∀ (m : ℕ),
    m < f → ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
n : ℕ
start rest : List Char
⊢ (match f, n, start ++ rest 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)) =
    (match f, n, start 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)) ++
      rest
Tactic:
split
State after:
case h.h_1
b : ℕ
start rest : List Char
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ),
    m < 0 → ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
⊢ start ++ rest = start ++ rest

case h.h_2
b : ℕ
start rest : List Char
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < succ fuel✝ →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
⊢ (let d := digitChar (x✝³ % b);
    let n' := x✝³ / b;
    if n' = 0 then d :: (start ++ rest) else toDigitsCore b fuel✝ n' (d :: (start ++ rest))) =
    (let d := digitChar (x✝³ % b);
      let n' := x✝³ / b;
      if n' = 0 then d :: start else toDigitsCore b fuel✝ n' (d :: start)) ++
      rest

State before:
case h.h_1
b : ℕ
start rest : List Char
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ),
    m < 0 → ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
⊢ start ++ rest = start ++ rest

case h.h_2
b : ℕ
start rest : List Char
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < succ fuel✝ →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
⊢ (let d := digitChar (x✝³ % b);
    let n' := x✝³ / b;
    if n' = 0 then d :: (start ++ rest) else toDigitsCore b fuel✝ n' (d :: (start ++ rest))) =
    (let d := digitChar (x✝³ % b);
      let n' := x✝³ / b;
      if n' = 0 then d :: start else toDigitsCore b fuel✝ n' (d :: start)) ++
      rest
Tactic:
. case h.h_1 => simp
State after:
case h.h_2
b : ℕ
start rest : List Char
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < succ fuel✝ →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
⊢ (let d := digitChar (x✝³ % b);
    let n' := x✝³ / b;
    if n' = 0 then d :: (start ++ rest) else toDigitsCore b fuel✝ n' (d :: (start ++ rest))) =
    (let d := digitChar (x✝³ % b);
      let n' := x✝³ / b;
      if n' = 0 then d :: start else toDigitsCore b fuel✝ n' (d :: start)) ++
      rest

State before:
case h.h_2
b : ℕ
start rest : List Char
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < succ fuel✝ →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
⊢ (let d := digitChar (x✝³ % b);
    let n' := x✝³ / b;
    if n' = 0 then d :: (start ++ rest) else toDigitsCore b fuel✝ n' (d :: (start ++ rest))) =
    (let d := digitChar (x✝³ % b);
      let n' := x✝³ / b;
      if n' = 0 then d :: start else toDigitsCore b fuel✝ n' (d :: start)) ++
      rest
Tactic:
. case h.h_2 f _ _ _ q =>
  simp
  split
  . case inl =>
    simp
  . case inr =>
    rewrite [← List.cons_append]
    rewrite [ih]
    . rfl
    . simp only [lt_succ_self]
State after:
no goals

State before:
b : ℕ
start rest : List Char
x✝³ x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ),
    m < 0 → ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
⊢ start ++ rest = start ++ rest
Tactic:
simp
State after:
no goals

State before:
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
⊢ (let d := digitChar (f % b);
    let n' := f / b;
    if n' = 0 then d :: (start ++ rest) else toDigitsCore b q n' (d :: (start ++ rest))) =
    (let d := digitChar (f % b);
      let n' := f / b;
      if n' = 0 then d :: start else toDigitsCore b q n' (d :: start)) ++
      rest
Tactic:
simp
State after:
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
⊢ (if f / b = 0 then digitChar (f % b) :: (start ++ rest)
    else toDigitsCore b q (f / b) (digitChar (f % b) :: (start ++ rest))) =
    (if f / b = 0 then digitChar (f % b) :: start else toDigitsCore b q (f / b) (digitChar (f % b) :: start)) ++ rest

State before:
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
⊢ (if f / b = 0 then digitChar (f % b) :: (start ++ rest)
    else toDigitsCore b q (f / b) (digitChar (f % b) :: (start ++ rest))) =
    (if f / b = 0 then digitChar (f % b) :: start else toDigitsCore b q (f / b) (digitChar (f % b) :: start)) ++ rest
Tactic:
split
State after:
case inl
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : f / b = 0
⊢ digitChar (f % b) :: (start ++ rest) = digitChar (f % b) :: start ++ rest

case inr
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ toDigitsCore b q (f / b) (digitChar (f % b) :: (start ++ rest)) =
    toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest

State before:
case inl
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : f / b = 0
⊢ digitChar (f % b) :: (start ++ rest) = digitChar (f % b) :: start ++ rest

case inr
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ toDigitsCore b q (f / b) (digitChar (f % b) :: (start ++ rest)) =
    toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest
Tactic:
. case inl =>
  simp
State after:
case inr
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ toDigitsCore b q (f / b) (digitChar (f % b) :: (start ++ rest)) =
    toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest

State before:
case inr
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ toDigitsCore b q (f / b) (digitChar (f % b) :: (start ++ rest)) =
    toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest
Tactic:
. case inr =>
  rewrite [← List.cons_append]
  rewrite [ih]
  . rfl
  . simp only [lt_succ_self]
State after:
no goals

State before:
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : f / b = 0
⊢ digitChar (f % b) :: (start ++ rest) = digitChar (f % b) :: start ++ rest
Tactic:
simp
State after:
no goals

State before:
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ toDigitsCore b q (f / b) (digitChar (f % b) :: (start ++ rest)) =
    toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest
Tactic:
rewrite [← List.cons_append]
State after:
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ toDigitsCore b q (f / b) (digitChar (f % b) :: start ++ rest) =
    toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest

State before:
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ toDigitsCore b q (f / b) (digitChar (f % b) :: start ++ rest) =
    toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest
Tactic:
rewrite [ih]
State after:
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest =
    toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest

case a
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ q < succ q

State before:
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest =
    toDigitsCore b q (f / b) (digitChar (f % b) :: start) ++ rest

case a
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ q < succ q
Tactic:
. rfl
State after:
case a
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ q < succ q

State before:
case a
b : ℕ
start rest : List Char
f x✝² x✝¹ : ℕ
x✝ : List Char
q : ℕ
ih :
  ∀ (m : ℕ),
    m < succ q →
      ∀ {n : ℕ} {start rest : List Char}, toDigitsCore b m n (start ++ rest) = toDigitsCore b m n start ++ rest
h✝ : ¬f / b = 0
⊢ q < succ q
Tactic:
. simp only [lt_succ_self]
State after:
no goals