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₂ : 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:
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 true
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)
h₃ : (n / b == 0) = true
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
have h₄:n/b = 0 := by apply LawfulBEq.eq_of_beq; assumption
Proof state after:
case true
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)
h₃ : (n / b == 0) = true
h₄ : n / b = 0
⊢ Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case true
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)
h₃ : (n / b == 0) = true
h₄ : n / b = 0
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
simp [h₄] at h₂
Proof state after:
case true
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) = true
h₄ : n / b = 0
h₂ : c = digitChar (n % b) ∨ c ∈ a
⊢ Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case true
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) = true
h₄ : n / b = 0
h₂ : c = digitChar (n % b) ∨ c ∈ a
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
cases h₂ with
| inr h₅ => simp [h₅]
| inl h₅ =>
  left 
  rw [h₅]
  simp [nmodb_le10, Nat.digitChar_is_digit]
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₂ : c ∈ if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
h₃ : (n / b == 0) = true
⊢ n / b = 0
Tactic:
apply LawfulBEq.eq_of_beq
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
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)
h₃ : (n / b == 0) = true
⊢ (n / b == 0) = true
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
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)
h₃ : (n / b == 0) = true
⊢ (n / b == 0) = true
Tactic:
assumption
Proof state after:
no goals
Theorem: Nat.toDigitsCore_digits
Proof state before:
case true.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) = true
h₄ : n / b = 0
h₅ : c ∈ a
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
simp [h₅]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_digits
Proof state before:
case true.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) = true
h₄ : n / b = 0
h₅ : c = digitChar (n % b)
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
left
Proof state after:
case true.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) = true
h₄ : n / b = 0
h₅ : c = digitChar (n % b)
⊢ Char.isDigit c = true
Theorem: Nat.toDigitsCore_digits
Proof state before:
case true.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) = true
h₄ : n / b = 0
h₅ : c = digitChar (n % b)
⊢ Char.isDigit c = true
Tactic:
rw [h₅]
Proof state after:
case true.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) = true
h₄ : n / b = 0
h₅ : c = digitChar (n % b)
⊢ Char.isDigit (digitChar (n % b)) = true
Theorem: Nat.toDigitsCore_digits
Proof state before:
case true.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) = true
h₄ : n / b = 0
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
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)
h₃ : (n / b == 0) = false
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
have h₄: n/b ≠ 0 := by apply ne_of_beq_false; assumption
Proof state after:
case false
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)
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
⊢ Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case false
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)
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
simp [h₄] at h₂
Proof state after:
case false
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)
⊢ Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case false
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)
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
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₂
Proof state after:
case false
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 ∨ c ∈ digitChar (n % b) :: a
⊢ Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case false
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 ∨ c ∈ digitChar (n % b) :: a
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
simp at h₅
Proof state after:
case false
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 ∨ c = digitChar (n % b) ∨ c ∈ a
⊢ Char.isDigit c = true ∨ c ∈ a
Theorem: Nat.toDigitsCore_digits
Proof state before:
case false
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 ∨ c = digitChar (n % b) ∨ c ∈ a
⊢ Char.isDigit c = true ∨ c ∈ a
Tactic:
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
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)
h₃ : (n / b == 0) = false
⊢ n / b ≠ 0
Tactic:
apply ne_of_beq_false
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
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)
h₃ : (n / b == 0) = false
⊢ (n / b == 0) = false
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
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)
h₃ : (n / b == 0) = false
⊢ (n / b == 0) = false
Tactic:
assumption
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)
⊢ Char.isDigit c = true ∨ c ∈ digitChar (n % b) :: a
Tactic:
apply h (n/b) (f:= fuel) (a:=(Nat.digitChar (n % b) :: a))
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
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)
⊢ n / b < n

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
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)
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
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)
⊢ n / b < n

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
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:
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]
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
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)
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
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:
next _ => exact 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 : ℕ
h₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
⊢ n / b < n
Tactic:
have h₅: n ≠ 0 := by 
  intro x
  unfold Ne at h₄
  have h₆:= Nat.zero_div b
  conv at h₆ =>
    left
    rw [← x]
  contradiction
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₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
h₅ : n ≠ 0
⊢ n / b < n
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)
h₅ : n ≠ 0
⊢ n / b < n
Tactic:
apply Nat.div_lt_self
Proof state after:
case hLtN
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₅ : n ≠ 0
⊢ 0 < n

case hLtK
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₅ : n ≠ 0
⊢ 1 < b
Theorem: Nat.toDigitsCore_digits
Proof state before:
case hLtN
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₅ : n ≠ 0
⊢ 0 < n

case hLtK
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₅ : n ≠ 0
⊢ 1 < b
Tactic:
. simp [h₅, Nat.pos_of_ne_zero]
Proof state after:
case hLtK
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₅ : n ≠ 0
⊢ 1 < b
Theorem: Nat.toDigitsCore_digits
Proof state before:
case hLtK
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₅ : n ≠ 0
⊢ 1 < b
Tactic:
. simp [Q]
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)
⊢ n ≠ 0
Tactic:
intro x
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₃ : (n / b == 0) = false
h₄ : n / b ≠ 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
x : n = 0
⊢ False
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
⊢ False
Tactic:
unfold Ne at 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₃ : (n / b == 0) = false
h₄ : ¬n / b = 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
x : n = 0
⊢ False
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
⊢ False
Tactic:
have h₆:= Nat.zero_div b
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₃ : (n / b == 0) = false
h₄ : ¬n / b = 0
h₂ : c ∈ toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)
x : n = 0
h₆ : 0 / b = 0
⊢ False
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₆ : 0 / b = 0
⊢ False
Tactic:
conv at h₆ =>
  left
  rw [← x]
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₃ : (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