internlm/Lean-Github huggingface dataset:
Theorem: Nat.toDigitsCore_digits
Proof state before:
c : Char
b : ℕ
P : b ≤ 10
Q : b > 1
n : ℕ
h : ∀ (m : ℕ), m < n → ∀ {f : ℕ} {a : List Char}, c ∈ toDigitsCore b f m a → Char.isDigit c = true ∨ c ∈ a
a : List Char
x✝³ : b > 0
nmodb_le10 : n % b < 10
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
h₃ : (n / b == 0) = false
h₄ : ¬n / b = 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
x : n = 0
h₆ : n / b = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.toDigitsCore_digits
Proof state before:
c : Char
b : ℕ
P : b ≤ 10
Q : b > 1
n : ℕ
h : ∀ (m : ℕ), m < n → ∀ {f : ℕ} {a : List Char}, c ∈ toDigitsCore b f m a → Char.isDigit c = true ∨ c ∈ a
a : List Char
x✝³ : b > 0
nmodb_le10 : n % b < 10
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
⊢ c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Nat.toDigitsCore_digits
Proof state before:
case false.inl
c : Char
b : ℕ
P : b ≤ 10
Q : b > 1
n : ℕ
h : ∀ (m : ℕ), m < n → ∀ {f : ℕ} {a : List Char}, c ∈ toDigitsCore b f m a → Char.isDigit c = true ∨ c ∈ a
a : List Char
x✝³ : b > 0
nmodb_le10 : n % b < 10
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
h₆ : Char.isDigit c = true
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
simp [h₆]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_digits
Proof state before:
case false.inr
c : Char
b : ℕ
P : b ≤ 10
Q : b > 1
n : ℕ
h : ∀ (m : ℕ), m < n → ∀ {f : ℕ} {a : List Char}, c ∈ toDigitsCore b f m a → Char.isDigit c = true ∨ c ∈ a
a : List Char
x✝³ : b > 0
nmodb_le10 : n % b < 10
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
h₆ : c = digitChar (n % b) ∨ c ∈ a
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
cases h₆ with
| inl h₇ => rw [h₇]; left; simp [nmodb_le10, Nat.digitChar_is_digit]
| inr h₇ => simp [h₇]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_digits
Proof state before:
case false.inr.inl
c : Char
b : ℕ
P : b ≤ 10
Q : b > 1
n : ℕ
h : ∀ (m : ℕ), m < n → ∀ {f : ℕ} {a : List Char}, c ∈ toDigitsCore b f m a → Char.isDigit c = true ∨ c ∈ a
a : List Char
x✝³ : b > 0
nmodb_le10 : n % b < 10
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
h₇ : c = digitChar (n % b)
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
rw [h₇]
Proof state after:
case false.inr.inl
c : Char
b : ℕ
P : b ≤ 10
Q : b > 1
n : ℕ
h : ∀ (m : ℕ), m < n → ∀ {f : ℕ} {a : List Char}, c ∈ toDigitsCore b f m a → Char.isDigit c = true ∨ c ∈ a
a : List Char
x✝³ : b > 0
nmodb_le10 : n % b < 10
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
h₇ : c = digitChar (n % b)
⊢ Char.isDigit (digitChar (n % b)) = true ∨ digitChar (n % b) ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case false.inr.inl
c : Char
b : ℕ
P : b ≤ 10
Q : b > 1
n : ℕ
h : ∀ (m : ℕ), m < n → ∀ {f : ℕ} {a : List Char}, c ∈ toDigitsCore b f m a → Char.isDigit c = true ∨ c ∈ a
a : List Char
x✝³ : b > 0
nmodb_le10 : n % b < 10
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
h₇ : c = digitChar (n % b)
⊢ Char.isDigit (digitChar (n % b)) = true ∨ digitChar (n % b) ∈ a
Tactic:
left
Proof state after:
case false.inr.inl.h
c : Char
b : ℕ
P : b ≤ 10
Q : b > 1
n : ℕ
h : ∀ (m : ℕ), m < n → ∀ {f : ℕ} {a : List Char}, c ∈ toDigitsCore b f m a → Char.isDigit c = true ∨ c ∈ a
a : List Char
x✝³ : b > 0
nmodb_le10 : n % b < 10
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
h₇ : c = digitChar (n % b)
⊢ Char.isDigit (digitChar (n % b)) = true
Theorem: Nat.toDigitsCore_digits
Proof state before:
case false.inr.inl.h
c : Char
b : ℕ
P : b ≤ 10
Q : b > 1
n : ℕ
h : ∀ (m : ℕ), m < n → ∀ {f : ℕ} {a : List Char}, c ∈ toDigitsCore b f m a → Char.isDigit c = true ∨ c ∈ a
a : List Char
x✝³ : b > 0
nmodb_le10 : n % b < 10
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
h₇ : c = digitChar (n % b)
⊢ Char.isDigit (digitChar (n % b)) = true
Tactic:
simp [nmodb_le10, Nat.digitChar_is_digit]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_digits
Proof state before:
case false.inr.inr
c : Char
b : ℕ
P : b ≤ 10
Q : b > 1
n : ℕ
h : ∀ (m : ℕ), m < n → ∀ {f : ℕ} {a : List Char}, c ∈ toDigitsCore b f m a → Char.isDigit c = true ∨ c ∈ a
a : List Char
x✝³ : b > 0
nmodb_le10 : n % b < 10
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
h₇ : c ∈ a
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
simp [h₇]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_accumulates
Proof 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]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_accumulates
Proof 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
Proof 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
Theorem: Nat.toDigitsCore_accumulates
Proof 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
Proof 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
Theorem: Nat.toDigitsCore_accumulates
Proof 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
Proof 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
Theorem: Nat.toDigitsCore_accumulates
Proof 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]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_accumulates
Proof 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
Proof state after:
no goals
Theorem: Nat.toDigitsCore_accumulates
Proof 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
Proof 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
Theorem: Nat.toDigitsCore_accumulates
Proof 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
Proof 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
Theorem: Nat.toDigitsCore_accumulates
Proof 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
Proof 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
Theorem: Nat.toDigitsCore_accumulates
Proof 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]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_accumulates
Proof 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
Proof state after:
no goals
Theorem: Nat.toDigitsCore_accumulates
Proof 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]
Proof 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
Theorem: Nat.toDigitsCore_accumulates
Proof 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]
Proof 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
Theorem: Nat.toDigitsCore_accumulates
Proof 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
Proof 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
Theorem: Nat.toDigitsCore_accumulates
Proof 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]
Proof state after:
no goals
Theorem: Nat.todigitsCore_accumulates_suffix
Proof state before:
b f n : ℕ
rest : List Char
⊢ toDigitsCore b f n rest = toDigitsCore b f n [] ++ rest
Tactic:
have h: rest = [] ++ rest := by simp
Proof state after:
b f n : ℕ
rest : List Char
h : rest = [] ++ rest
⊢ toDigitsCore b f n rest = toDigitsCore b f n [] ++ rest
Theorem: Nat.todigitsCore_accumulates_suffix
Proof state before:
b f n : ℕ
rest : List Char
h : rest = [] ++ rest
⊢ toDigitsCore b f n rest = toDigitsCore b f n [] ++ rest
Tactic:
conv=> left; rw [h]
Proof state after:
b f n : ℕ
rest : List Char
h : rest = [] ++ rest
⊢ toDigitsCore b f n ([] ++ rest) = toDigitsCore b f n [] ++ rest
Theorem: Nat.todigitsCore_accumulates_suffix
Proof state before:
b f n : ℕ
rest : List Char
h : rest = [] ++ rest
⊢ toDigitsCore b f n ([] ++ rest) = toDigitsCore b f n [] ++ rest
Tactic:
apply Nat.toDigitsCore_accumulates
Proof state after:
no goals
Theorem: Nat.todigitsCore_accumulates_suffix
Proof state before:
b f n : ℕ
rest : List Char
⊢ rest = [] ++ rest
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
f n b : ℕ
rest : List Char
P : f ≥ n + 1
Q : b > 1
⊢ toDigitsCore b f n rest = toDigitsCore b (n + 1) n rest
Tactic:
induction f using Nat.strong_induction_on generalizing rest n
Proof state after:
case h
b : ℕ
Q : b > 1
n✝ : ℕ
a✝ :
  ∀ (m : ℕ), m < n✝ → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : n✝ ≥ n + 1
⊢ toDigitsCore b n✝ n rest = toDigitsCore b (n + 1) n rest
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
f : ℕ
ih :
  ∀ (m : ℕ), m < f → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : f ≥ n + 1
⊢ toDigitsCore b f n rest = toDigitsCore b (n + 1) n rest
Tactic:
case h f ih =>
  unfold toDigitsCore
  simp
  split
  case h_1 =>
    simp at P
  case h_2 n' =>
    conv =>
      left; rw [Nat.todigitsCore_accumulates_suffix]
    conv =>
      right; rw [Nat.todigitsCore_accumulates_suffix]
    split
    case inl =>
      rfl
    case inr =>
      simp
      rw [ih]
      .  cases h: n == (n / b) + 1 with
          | false => 
            simp at h
            rw [← Nat.toDigits, ih, ← Nat.toDigits]
            . calc
                succ n' ≥  n + 1 := P
                _ > n := by simp only [gt_iff_lt, lt_add_iff_pos_right]
            . simp [h]
              have h₂: n ≥  n / b + 1 := by 
                simp
                apply Nat.div_lt_self
                . apply Nat.pos_of_ne_zero; intro h; simp only [gt_iff_lt, h, Nat.zero_div, not_true] at *
                . exact Q
              simp [ge_iff_le] at h₂
              have h₃:= Nat.eq_or_lt_of_le h₂
              cases h₃ with
              | inl h₄ => exfalso; apply h; simp only [h₄]
              | inr h₄ => exact h₂
          | true => 
            simp at h
            rw [← h]
      . simp
      . simp [Nat.succ_eq_add_one] at P 
        calc
          n' ≥  n        := P
          n ≥ n / b + 1 := by simp only [add_lt_add_iff_right]; apply Nat.div_lt_self; apply Nat.pos_of_ne_zero; intro h; simp only [gt_iff_lt, h, Nat.zero_div, not_true] at *; apply Q
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
f : ℕ
ih :
  ∀ (m : ℕ), m < f → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : f ≥ n + 1
⊢ toDigitsCore b f n rest = toDigitsCore b (n + 1) n rest
Tactic:
unfold toDigitsCore
Proof state after:
b : ℕ
Q : b > 1
f : ℕ
ih :
  ∀ (m : ℕ), m < f → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : f ≥ n + 1
⊢ (match f, n, 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)) =
    let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: rest else toDigitsCore b (Nat.add n 0) n' (d :: rest)
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
f : ℕ
ih :
  ∀ (m : ℕ), m < f → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : f ≥ n + 1
⊢ (match f, n, 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)) =
    let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: rest else toDigitsCore b (Nat.add n 0) n' (d :: rest)
Tactic:
simp
Proof state after:
b : ℕ
Q : b > 1
f : ℕ
ih :
  ∀ (m : ℕ), m < f → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : f ≥ n + 1
⊢ (match f, n, rest with
    | 0, x, ds => ds
    | succ fuel, n, ds =>
      if n / b = 0 then digitChar (n % b) :: ds else toDigitsCore b fuel (n / b) (digitChar (n % b) :: ds)) =
    if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) (digitChar (n % b) :: rest)