internlm/Lean-Github huggingface dataset:
Theorem: String.toNatAux_accumulates
Proof state before:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail 0 + (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail +
      accum * 10 ^ (List.length tail + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: String.toNatΔ_cons
Proof state before:
head : Char
tail : List Char
⊢ toNatΔ (head :: tail) = (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail + toNatΔ tail
Tactic:
unfold String.toNatΔ
Proof state after:
head : Char
tail : List Char
⊢ toNatAux (head :: tail) 0 = (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail + toNatAux tail 0
Theorem: String.toNatΔ_cons
Proof state before:
head : Char
tail : List Char
⊢ toNatAux (head :: tail) 0 = (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail + toNatAux tail 0
Tactic:
rw [String.toNatAux, String.toNatAux_accumulates]
Proof state after:
head : Char
tail : List Char
⊢ toNatAux tail 0 + (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail + toNatAux tail 0
Theorem: String.toNatΔ_cons
Proof state before:
head : Char
tail : List Char
⊢ toNatAux tail 0 + (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail + toNatAux tail 0
Tactic:
ring
Proof state after:
no goals
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
f n b : ℕ
a : List Char
P : f > n
⊢ toDigitsCore b f n a ≠ []
Tactic:
unfold Nat.toDigitsCore
Proof state after:
f n b : ℕ
a : List Char
P : f > n
⊢ (match f, n, a 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)) ≠
    []
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
f n b : ℕ
a : List Char
P : f > n
⊢ (match f, n, a 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)) ≠
    []
Tactic:
split
Proof state after:
case h_1
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
P : 0 > n
⊢ a ≠ []

case h_2
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ > n
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) ≠
    []
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
case h_1
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
P : 0 > n
⊢ a ≠ []

case h_2
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ > n
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) ≠
    []
Tactic:
. case _ => contradiction
Proof state after:
case h_2
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ > n
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) ≠
    []
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
case h_2
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ > n
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) ≠
    []
Tactic:
. case _ _ _ _ fuel =>
  simp
  have h: ∀x, List.length (Nat.toDigitsCore b fuel (n / b) (x :: a)) ≠ 0 := by
    simp [Nat.to_digits_core_lens_eq]
  split
  case _ => simp
  case _ => 
    intro P₂
    apply h
    rw [P₂]
    simp
Proof state after:
no goals
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
P : 0 > n
⊢ a ≠ []
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: a else toDigitsCore b fuel n' (d :: a)) ≠
    []
Tactic:
simp
Proof state after:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
⊢ ¬(if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)) = []
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
⊢ ¬(if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)) = []
Tactic:
have h: ∀x, List.length (Nat.toDigitsCore b fuel (n / b) (x :: a)) ≠ 0 := by
  simp [Nat.to_digits_core_lens_eq]
Proof state after:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
⊢ ¬(if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)) = []
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
⊢ ¬(if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)) = []
Tactic:
split
Proof state after:
case inl
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : n / b = 0
⊢ ¬False

case inr
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
⊢ ¬toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : n / b = 0
⊢ ¬False
Tactic:
case _ => simp
Proof state after:
no goals
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
⊢ ¬toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
Tactic:
case _ => 
  intro P₂
  apply h
  rw [P₂]
  simp
Proof state after:
no goals
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
⊢ ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
Tactic:
simp [Nat.to_digits_core_lens_eq]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : n / b = 0
⊢ ¬False
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
⊢ ¬toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
Tactic:
intro P₂
Proof state after:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ False
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ False
Tactic:
apply h
Proof state after:
case a
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ List.length (toDigitsCore b fuel (n / b) (?x :: a)) = 0

case x
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ Char
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
case a
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ List.length (toDigitsCore b fuel (n / b) (?x :: a)) = 0

case x
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ Char
Tactic:
rw [P₂]
Proof state after:
case a
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ List.length [] = 0
Theorem: Nat.toDigitsCore_ne_nil
Proof state before:
case a
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ List.length [] = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.toDigits_ne_nil
Proof state before:
b n : ℕ
⊢ toDigits b n ≠ []
Tactic:
unfold Nat.toDigits
Proof state after:
b n : ℕ
⊢ toDigitsCore b (n + 1) n [] ≠ []
Theorem: Nat.toDigits_ne_nil
Proof state before:
b n : ℕ
⊢ toDigitsCore b (n + 1) n [] ≠ []
Tactic:
simp [Nat.toDigitsCore_ne_nil]
Proof state after:
no goals
Theorem: Int.reprΔ_ne_nil
Proof state before:
i : ℤ
⊢ reprΔ i ≠ []
Tactic:
unfold Int.reprΔ
Proof state after:
i : ℤ
⊢ (match i with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)) ≠
    []
Theorem: Int.reprΔ_ne_nil
Proof state before:
i : ℤ
⊢ (match i with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)) ≠
    []
Tactic:
cases i with
| ofNat m => simp only; apply Nat.toDigits_ne_nil
| negSucc m => simp only [List.singleton_append, ne_eq, not_false_iff]
Proof state after:
no goals
Theorem: Int.reprΔ_ne_nil
Proof state before:
case ofNat
m : ℕ
⊢ (match ofNat m with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)) ≠
    []
Tactic:
simp only
Proof state after:
case ofNat
m : ℕ
⊢ Nat.toDigits 10 m ≠ []
Theorem: Int.reprΔ_ne_nil
Proof state before:
case ofNat
m : ℕ
⊢ Nat.toDigits 10 m ≠ []
Tactic:
apply Nat.toDigits_ne_nil
Proof state after:
no goals
Theorem: Int.reprΔ_ne_nil
Proof state before:
case negSucc
m : ℕ
⊢ (match -[m+1] with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)) ≠
    []
Tactic:
simp only [List.singleton_append, ne_eq, not_false_iff]
Proof state after:
no goals
Theorem: Nat.digitChar_is_digit
Proof state before:
n : ℕ
P : n < 10
⊢ Char.isDigit (digitChar n) = true
Tactic:
revert n
Proof state after:
⊢ ∀ (n : ℕ), n < 10 → Char.isDigit (digitChar n) = true
Theorem: Nat.digitChar_is_digit
Proof state before:
⊢ ∀ (n : ℕ), n < 10 → Char.isDigit (digitChar n) = true
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.toDigitsCore_digits
Proof state before:
c : Char
f : ℕ
a : List Char
b n : ℕ
P : b ≤ 10
Q : b > 1
⊢ c ∈ toDigitsCore b f n a → Char.isDigit c = true ∨ c ∈ a
Tactic:
induction n using Nat.strong_induction_on generalizing f a with
| _ n h =>
  have _: b>0 := by calc
          b > 1 := Q
          _ > 0 := by simp
  have nmodb_le10: n % b < 10 := by calc
    n % b < b  := by apply Nat.mod_lt;  simp [*]
    _     ≤ 10 := by exact P
  unfold Nat.toDigitsCore
  split
  next =>
    intro h₂
    simp [h₂]
  next _ _ _ fuel=>
    simp
    intro h₂
    cases h₃: n / b == 0 with
    | true =>
      have h₄:n/b = 0 := by apply LawfulBEq.eq_of_beq; assumption
      simp [h₄] at h₂
      cases h₂ with
      | inr h₅ => simp [h₅]
      | inl h₅ =>
        left 
        rw [h₅]
        simp [nmodb_le10, Nat.digitChar_is_digit]
    | false =>
      have h₄: n/b ≠ 0 := by apply ne_of_beq_false; assumption
      simp [h₄] at h₂
      have h₅: Char.isDigit c = true ∨ c ∈ Nat.digitChar (n % b) :: a := by
        apply h (n/b) (f:= fuel) (a:=(Nat.digitChar (n % b) :: a))
        next =>
          have h₅: n ≠ 0 := by 
            intro x
            unfold Ne at h₄
            have h₆:= Nat.zero_div b
            conv at h₆ =>
              left
              rw [← x]
            contradiction
          apply Nat.div_lt_self
          . simp [h₅, Nat.pos_of_ne_zero]
          . simp [Q]
        next _ => exact h₂
      simp at h₅
      cases h₅ with
      | inl h₆ => simp [h₆]
      | inr h₆ => 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 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
f : ℕ
a : List Char
⊢ c ∈ toDigitsCore b f n a → Char.isDigit c = true ∨ c ∈ a
Tactic:
have _: b>0 := by calc
        b > 1 := Q
        _ > 0 := by simp
Proof state after:
case 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
f : ℕ
a : List Char
x✝ : b > 0
⊢ c ∈ toDigitsCore b f n a → Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case 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
f : ℕ
a : List Char
x✝ : b > 0
⊢ c ∈ toDigitsCore b f n a → Char.isDigit c = true ∨ c ∈ a
Tactic:
have nmodb_le10: n % b < 10 := by calc
  n % b < b  := by apply Nat.mod_lt;  simp [*]
  _     ≤ 10 := by exact P
Proof state after:
case 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
f : ℕ
a : List Char
x✝ : b > 0
nmodb_le10 : n % b < 10
⊢ c ∈ toDigitsCore b f n a → Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case 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
f : ℕ
a : List Char
x✝ : b > 0
nmodb_le10 : n % b < 10
⊢ c ∈ toDigitsCore b f n a → Char.isDigit c = true ∨ c ∈ a
Tactic:
unfold Nat.toDigitsCore
Proof state after:
case 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
f : ℕ
a : List Char
x✝ : b > 0
nmodb_le10 : n % b < 10
⊢ (c ∈
      match f, n, a 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)) →
    Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case 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
f : ℕ
a : List Char
x✝ : b > 0
nmodb_le10 : n % b < 10
⊢ (c ∈
      match f, n, a 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)) →
    Char.isDigit c = true ∨ c ∈ a
Tactic:
split
Proof state after:
case h.h_1
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
⊢ c ∈ a → Char.isDigit c = true ∨ c ∈ a

case h.h_2
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✝ : ℕ
⊢ (c ∈
      let d := digitChar (n % b);
      let n' := n / b;
      if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) →
    Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case h.h_1
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
⊢ c ∈ a → Char.isDigit c = true ∨ c ∈ a

case h.h_2
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✝ : ℕ
⊢ (c ∈
      let d := digitChar (n % b);
      let n' := n / b;
      if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) →
    Char.isDigit c = true ∨ c ∈ a
Tactic:
next =>
  intro h₂
  simp [h₂]
Proof state after:
case h.h_2
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✝ : ℕ
⊢ (c ∈
      let d := digitChar (n % b);
      let n' := n / b;
      if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) →
    Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case h.h_2
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✝ : ℕ
⊢ (c ∈
      let d := digitChar (n % b);
      let n' := n / b;
      if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) →
    Char.isDigit c = true ∨ c ∈ a
Tactic:
next _ _ _ fuel=>
  simp
  intro h₂
  cases h₃: n / b == 0 with
  | true =>
    have h₄:n/b = 0 := by apply LawfulBEq.eq_of_beq; assumption
    simp [h₄] at h₂
    cases h₂ with
    | inr h₅ => simp [h₅]
    | inl h₅ =>
      left 
      rw [h₅]
      simp [nmodb_le10, Nat.digitChar_is_digit]
  | false =>
    have h₄: n/b ≠ 0 := by apply ne_of_beq_false; assumption
    simp [h₄] at h₂
    have h₅: Char.isDigit c = true ∨ c ∈ Nat.digitChar (n % b) :: a := by
      apply h (n/b) (f:= fuel) (a:=(Nat.digitChar (n % b) :: a))
      next =>
        have h₅: n ≠ 0 := by 
          intro x
          unfold Ne at h₄
          have h₆:= Nat.zero_div b
          conv at h₆ =>
            left
            rw [← x]
          contradiction
        apply Nat.div_lt_self
        . simp [h₅, Nat.pos_of_ne_zero]
        . simp [Q]
      next _ => exact h₂
    simp at h₅
    cases h₅ with
    | inl h₆ => simp [h₆]
    | inr h₆ => 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:
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
f : ℕ
a : List Char
⊢ b > 0
Tactic:
calc
b > 1 := Q
_ > 0 := by simp
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
f : ℕ
a : List Char
⊢ 1 > 0
Tactic:
simp
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
f : ℕ
a : List Char
x✝ : b > 0
⊢ n % b < 10
Tactic:
calc
n % b < b  := by apply Nat.mod_lt;  simp [*]
_     ≤ 10 := by exact P
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
f : ℕ
a : List Char
x✝ : b > 0
⊢ n % b < b
Tactic:
apply Nat.mod_lt
Proof state after:
case a
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
f : ℕ
a : List Char
x✝ : b > 0
⊢ b > 0
Theorem: Nat.toDigitsCore_digits
Proof state before:
case a
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
f : ℕ
a : List Char
x✝ : b > 0
⊢ b > 0
Tactic:
simp [*]
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
f : ℕ
a : List Char
x✝ : b > 0
⊢ b ≤ 10
Tactic:
exact P
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
⊢ c ∈ a → Char.isDigit c = true ∨ c ∈ a
Tactic:
intro h₂
Proof state after:
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
h₂ : c ∈ a
⊢ Char.isDigit c = true ∨ c ∈ a
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
h₂ : c ∈ a
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
simp [h₂]
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 : ℕ
⊢ (c ∈
      let d := digitChar (n % b);
      let n' := n / b;
      if n' = 0 then d :: a else toDigitsCore b fuel n' (d :: a)) →
    Char.isDigit c = true ∨ c ∈ a
Tactic:
simp
Proof state after:
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 : ℕ
⊢ (c ∈ if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)) →
    Char.isDigit c = true ∨ c ∈ a
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 : ℕ
⊢ (c ∈ if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)) →
    Char.isDigit c = true ∨ c ∈ a
Tactic:
intro h₂
Proof state after:
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₂ : c ∈ if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
⊢ Char.isDigit c = true ∨ c ∈ a