Theorem: Nat.toDigitsCore_digits (One.lean)

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₇]
State after:
no goals

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
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

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
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

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
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

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
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

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₂]
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

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₇]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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 [*]
State after:
no goals

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
State after:
no goals

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₂
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

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₂]
State after:
no goals

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
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

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₂
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

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₇]
State after:
no goals

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
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

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₂
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

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]
State after:
no goals

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
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

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
State after:
no goals

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₅]
State after:
no goals

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
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

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₅]
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

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]
State after:
no goals

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
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

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₂
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

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₂
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

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₅
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

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₇]
State after:
no goals

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
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

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
State after:
no goals

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))
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)

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]
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)

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₂
State after:
no goals

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
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

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
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

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]
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

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]
State after:
no goals

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
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

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₄
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

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
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

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]
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

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
State after:
no goals

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₂
State after:
no goals

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₆]
State after:
no goals

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₇]
State after:
no goals

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₇]
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

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
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

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]
State after:
no goals

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₇]
State after:
no goals