internlm/Lean-Github huggingface dataset:
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case false.P.inr
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
h₂ : n / b + 1 ≤ n
h₄ : n / b + 1 < n
⊢ n / b + 1 ≤ n
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case true
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : (n == n / b + 1) = true
⊢ toDigitsCore b (n / b + 1) (n / b) [] = toDigitsCore b n (n / b) []
Tactic:
simp at h
Proof state after:
case true
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : n = n / b + 1
⊢ toDigitsCore b (n / b + 1) (n / b) [] = toDigitsCore b n (n / b) []
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case true
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : n = n / b + 1
⊢ toDigitsCore b (n / b + 1) (n / b) [] = toDigitsCore b n (n / b) []
Tactic:
rw [← h]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ n ≥ n / b + 1
Tactic:
apply Nat.div_lt_self
Proof state after:
case hLtN
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 0 < n

case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case hLtN
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 0 < n

case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Tactic:
apply Nat.pos_of_ne_zero
Proof state after:
case hLtN.a
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ n ≠ 0

case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case hLtN.a
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ n ≠ 0

case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Tactic:
intro h
Proof state after:
case hLtN.a
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
h : n = 0
⊢ False

case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case hLtN.a
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
h : n = 0
⊢ False

case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Tactic:
simp only [gt_iff_lt, h, Nat.zero_div, not_true] at *
Proof state after:
case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Tactic:
apply Q
Proof state after:
no goals
Theorem: Nat.toDigits_digits
Proof state before:
b n : ℕ
P : b ≤ 10
Q : b > 1
⊢ (List.all (toDigits b n) Char.isDigit == true) = true
Tactic:
let h:  ∀ c, c ∈ Nat.toDigitsCore b (n+1) n [] → Char.isDigit c = true ∨ c ∈ [] := by
  intro c
  apply Nat.toDigitsCore_digits  _ _ P Q
Proof state after:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ [] :=
  fun c => toDigitsCore_digits b n P Q
⊢ (List.all (toDigits b n) Char.isDigit == true) = true
Theorem: Nat.toDigits_digits
Proof state before:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ [] :=
  fun c => toDigitsCore_digits b n P Q
⊢ (List.all (toDigits b n) Char.isDigit == true) = true
Tactic:
simp
Proof state after:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ [] :=
  fun c => toDigitsCore_digits b n P Q
⊢ ∀ (x : Char), x ∈ toDigits b n → Char.isDigit x = true
Theorem: Nat.toDigits_digits
Proof state before:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ [] :=
  fun c => toDigitsCore_digits b n P Q
⊢ ∀ (x : Char), x ∈ toDigits b n → Char.isDigit x = true
Tactic:
simp at h
Proof state after:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true
⊢ ∀ (x : Char), x ∈ toDigits b n → Char.isDigit x = true
Theorem: Nat.toDigits_digits
Proof state before:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true
⊢ ∀ (x : Char), x ∈ toDigits b n → Char.isDigit x = true
Tactic:
unfold Nat.toDigits
Proof state after:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true
⊢ ∀ (x : Char), x ∈ toDigitsCore b (n + 1) n [] → Char.isDigit x = true
Theorem: Nat.toDigits_digits
Proof state before:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true
⊢ ∀ (x : Char), x ∈ toDigitsCore b (n + 1) n [] → Char.isDigit x = true
Tactic:
apply h
Proof state after:
no goals
Theorem: Nat.toDigits_digits
Proof state before:
b n : ℕ
P : b ≤ 10
Q : b > 1
⊢ ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ []
Tactic:
intro c
Proof state after:
b n : ℕ
P : b ≤ 10
Q : b > 1
c : Char
⊢ c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ []
Theorem: Nat.toDigits_digits
Proof state before:
b n : ℕ
P : b ≤ 10
Q : b > 1
c : Char
⊢ c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ []
Tactic:
apply Nat.toDigitsCore_digits  _ _ P Q
Proof state after:
no goals
Theorem: List.get?_cons
Proof state before:
α : Type u_1
h : α
tail : List α
n : ℕ
hn : n > 0
⊢ get? (h :: tail) n = get? tail (n - 1)
Tactic:
conv => left; unfold List.get?
Proof state after:
α : Type u_1
h : α
tail : List α
n : ℕ
hn : n > 0
⊢ (match h :: tail, n with
    | a :: tail, 0 => some a
    | head :: as, Nat.succ n => get? as n
    | x, x_1 => none) =
    get? tail (n - 1)
Theorem: List.get?_cons
Proof state before:
α : Type u_1
h : α
tail : List α
n : ℕ
hn : n > 0
⊢ (match h :: tail, n with
    | a :: tail, 0 => some a
    | head :: as, Nat.succ n => get? as n
    | x, x_1 => none) =
    get? tail (n - 1)
Tactic:
cases n with
| zero => simp only at hn
| succ n => simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub, nonpos_iff_eq_zero, tsub_zero]
Proof state after:
no goals
Theorem: List.get?_cons
Proof state before:
case zero
α : Type u_1
h : α
tail : List α
hn : Nat.zero > 0
⊢ (match h :: tail, Nat.zero with
    | a :: tail, 0 => some a
    | head :: as, Nat.succ n => get? as n
    | x, x_1 => none) =
    get? tail (Nat.zero - 1)
Tactic:
simp only at hn
Proof state after:
no goals
Theorem: List.get?_cons
Proof state before:
case succ
α : Type u_1
h : α
tail : List α
n : ℕ
hn : Nat.succ n > 0
⊢ (match h :: tail, Nat.succ n with
    | a :: tail, 0 => some a
    | head :: as, Nat.succ n => get? as n
    | x, x_1 => none) =
    get? tail (Nat.succ n - 1)
Tactic:
simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub, nonpos_iff_eq_zero, tsub_zero]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
⊢ ∀ (i : ℕ),
    List.getD (List.reverse (toDigits b n)) (i + 1) (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
intro i
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b n)) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b n)) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
rw [toDigits, toDigitsCore]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD
      (List.reverse
        (let d := digitChar (n % b);
        let n' := n / b;
        if n' = 0 then [d] else toDigitsCore b n n' [d]))
      (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD
      (List.reverse
        (let d := digitChar (n % b);
        let n' := n / b;
        if n' = 0 then [d] else toDigitsCore b n n' [d]))
      (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
simp only [add_eq, add_zero]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b n (n / b) [digitChar (n % b)]))
      (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b n (n / b) [digitChar (n % b)]))
      (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
split
Proof state after:
case inl
b n : ℕ
P : b > 1
i : ℕ
h✝ : n / b = 0
⊢ List.getD (List.reverse [digitChar (n % b)]) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

case inr
b n : ℕ
P : b > 1
i : ℕ
h✝ : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
case inl
b n : ℕ
P : b > 1
i : ℕ
h✝ : n / b = 0
⊢ List.getD (List.reverse [digitChar (n % b)]) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

case inr
b n : ℕ
P : b > 1
i : ℕ
h✝ : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
. next heq =>
  conv => left; unfold List.getD
  simp only [List.get?, Option.getD_none]
  rw [heq]
  unfold toDigits toDigitsCore digitChar
  simp only [Nat.zero_div, zero_mod, zero_ne_one, ite_false, ite_true, List.reverse_cons, List.reverse_nil,
List.nil_append, List.getD_singleton_default_eq]
Proof state after:
case inr
b n : ℕ
P : b > 1
i : ℕ
h✝ : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
case inr
b n : ℕ
P : b > 1
i : ℕ
h✝ : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
. next heq =>
  rw [Nat.todigitsCore_accumulates_suffix]
  rw [List.getD, List.getD]
  congr 1
  simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append,
    List.cons.injEq, succ.injEq, and_imp, forall_apply_eq_imp_iff₂, forall_apply_eq_imp_iff', forall_eq', 
    List.get?, add_eq, add_zero]
  rw [Nat.toDigitsCore_fuel_irrelevant, ← Nat.toDigits]
  . simp only [ge_iff_le]
    have h: n ≠ 0 := by 
      simp only [ne_eq]
      intro h
      rw [h] at heq
      simp only [Nat.zero_div] at heq
    apply Nat.div_lt_self
    . simp only [ne_eq, h, not_false_iff, Nat.pos_of_ne_zero]
    . exact P
  . exact P
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ List.getD (List.reverse [digitChar (n % b)]) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
conv => left; unfold List.getD
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Option.getD (List.get? (List.reverse [digitChar (n % b)]) (i + 1)) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Option.getD (List.get? (List.reverse [digitChar (n % b)]) (i + 1)) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
simp only [List.get?, Option.getD_none]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 = List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 = List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
rw [heq]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 = List.getD (List.reverse (toDigits b 0)) i (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 = List.getD (List.reverse (toDigits b 0)) i (Char.ofNat 48)
Tactic:
unfold toDigits toDigitsCore digitChar
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 =
    List.getD
      (List.reverse
        (let d :=
          if 0 % b = 0 then Char.ofNat 48
          else
            if 0 % b = 1 then Char.ofNat 49
            else
              if 0 % b = 2 then Char.ofNat 50
              else
                if 0 % b = 3 then Char.ofNat 51
                else
                  if 0 % b = 4 then Char.ofNat 52
                  else
                    if 0 % b = 5 then Char.ofNat 53
                    else
                      if 0 % b = 6 then Char.ofNat 54
                      else
                        if 0 % b = 7 then Char.ofNat 55
                        else
                          if 0 % b = 8 then Char.ofNat 56
                          else
                            if 0 % b = 9 then Char.ofNat 57
                            else
                              if 0 % b = 10 then Char.ofNat 97
                              else
                                if 0 % b = 11 then Char.ofNat 98
                                else
                                  if 0 % b = 12 then Char.ofNat 99
                                  else
                                    if 0 % b = 13 then Char.ofNat 100
                                    else
                                      if 0 % b = 14 then Char.ofNat 101
                                      else if 0 % b = 15 then Char.ofNat 102 else Char.ofNat 42;
        let n' := 0 / b;
        if n' = 0 then [d] else toDigitsCore b 0 n' [d]))
      i (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 =
    List.getD
      (List.reverse
        (let d :=
          if 0 % b = 0 then Char.ofNat 48
          else
            if 0 % b = 1 then Char.ofNat 49
            else
              if 0 % b = 2 then Char.ofNat 50
              else
                if 0 % b = 3 then Char.ofNat 51
                else
                  if 0 % b = 4 then Char.ofNat 52
                  else
                    if 0 % b = 5 then Char.ofNat 53
                    else
                      if 0 % b = 6 then Char.ofNat 54
                      else
                        if 0 % b = 7 then Char.ofNat 55
                        else
                          if 0 % b = 8 then Char.ofNat 56
                          else
                            if 0 % b = 9 then Char.ofNat 57
                            else
                              if 0 % b = 10 then Char.ofNat 97
                              else
                                if 0 % b = 11 then Char.ofNat 98
                                else
                                  if 0 % b = 12 then Char.ofNat 99
                                  else
                                    if 0 % b = 13 then Char.ofNat 100
                                    else
                                      if 0 % b = 14 then Char.ofNat 101
                                      else if 0 % b = 15 then Char.ofNat 102 else Char.ofNat 42;
        let n' := 0 / b;
        if n' = 0 then [d] else toDigitsCore b 0 n' [d]))
      i (Char.ofNat 48)
Tactic:
simp only [Nat.zero_div, zero_mod, zero_ne_one, ite_false, ite_true, List.reverse_cons, List.reverse_nil,
List.nil_append, List.getD_singleton_default_eq]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
rw [Nat.todigitsCore_accumulates_suffix]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
rw [List.getD, List.getD]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ Option.getD (List.get? (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1)) (Char.ofNat 48) =
    Option.getD (List.get? (List.reverse (toDigits b (n / b))) i) (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ Option.getD (List.get? (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1)) (Char.ofNat 48) =
    Option.getD (List.get? (List.reverse (toDigits b (n / b))) i) (Char.ofNat 48)
Tactic:
congr 1
Proof state after:
case e_a
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.get? (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1) =
    List.get? (List.reverse (toDigits b (n / b))) i
Theorem: Nat.toDigitsCore_shift'
Proof state before:
case e_a
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.get? (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1) =
    List.get? (List.reverse (toDigits b (n / b))) i
Tactic:
simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append,
  List.cons.injEq, succ.injEq, and_imp, forall_apply_eq_imp_iff₂, forall_apply_eq_imp_iff', forall_eq', 
  List.get?, add_eq, add_zero]
Proof state after:
case e_a
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.get? (List.reverse (toDigitsCore b n (n / b) [])) i = List.get? (List.reverse (toDigits b (n / b))) i
Theorem: Nat.toDigitsCore_shift'
Proof state before:
case e_a
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.get? (List.reverse (toDigitsCore b n (n / b) [])) i = List.get? (List.reverse (toDigits b (n / b))) i
Tactic:
rw [Nat.toDigitsCore_fuel_irrelevant, ← Nat.toDigits]
Proof state after:
case e_a.P
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ n ≥ n / b + 1

case e_a.Q
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ b > 1
Theorem: Nat.toDigitsCore_shift'
Proof state before:
case e_a.P
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ n ≥ n / b + 1

case e_a.Q
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ b > 1
Tactic:
. simp only [ge_iff_le]
  have h: n ≠ 0 := by 
    simp only [ne_eq]
    intro h
    rw [h] at heq
    simp only [Nat.zero_div] at heq
  apply Nat.div_lt_self
  . simp only [ne_eq, h, not_false_iff, Nat.pos_of_ne_zero]
  . exact P
Proof state after:
case e_a.Q
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ b > 1
Theorem: Nat.toDigitsCore_shift'
Proof state before:
case e_a.Q
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ b > 1
Tactic:
. exact P
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ n ≠ 0
Tactic:
simp only [ne_eq]
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ ¬n = 0
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ ¬n = 0
Tactic:
intro h
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
h : n = 0
⊢ False
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
h : n = 0
⊢ False
Tactic:
rw [h] at heq
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬0 / b = 0
h : n = 0
⊢ False
Theorem: Nat.toDigitsCore_shift'
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬0 / b = 0
h : n = 0
⊢ False
Tactic:
simp only [Nat.zero_div] at heq
Proof state after:
no goals
Theorem: Nat.toDigitsCore_shift
Proof state before:
b n : ℕ
P : b > 1
⊢ ∀ (i : ℕ),
    i > 0 →
      List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
        List.getD (List.reverse (toDigits b (n / b))) (i - 1) (Char.ofNat 48)
Tactic:
intro i igt
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) (i - 1) (Char.ofNat 48)
Theorem: Nat.toDigitsCore_shift
Proof state before:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) (i - 1) (Char.ofNat 48)
Tactic:
generalize h: i - 1 = p
Proof state after:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) p (Char.ofNat 48)