internlm/Lean-Github huggingface dataset:
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 =>
      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)
Tactic:
split
Proof state after:
case h_1
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ), m < 0 → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : 0 ≥ n + 1
⊢ rest = if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) (digitChar (n % b) :: rest)

case h_2
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < succ fuel✝ → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ fuel✝ ≥ n + 1
⊢ (if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b fuel✝ (n / b) (digitChar (n % b) :: rest)) =
    if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) (digitChar (n % b) :: rest)
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ), m < 0 → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : 0 ≥ n + 1
⊢ rest = if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) (digitChar (n % b) :: rest)
Tactic:
case h_1 =>
  simp at P
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
⊢ (if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n' (n / b) (digitChar (n % b) :: rest)) =
    if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) (digitChar (n % b) :: rest)
Tactic:
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
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
ih :
  ∀ (m : ℕ), m < 0 → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : 0 ≥ n + 1
⊢ rest = if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) (digitChar (n % b) :: rest)
Tactic:
simp at P
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
⊢ (if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n' (n / b) (digitChar (n % b) :: rest)) =
    if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) (digitChar (n % b) :: rest)
Tactic:
conv =>
  left; rw [Nat.todigitsCore_accumulates_suffix]
Proof state after:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
⊢ (if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n' (n / b) [] ++ digitChar (n % b) :: rest) =
    if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) (digitChar (n % b) :: rest)
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
⊢ (if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n' (n / b) [] ++ digitChar (n % b) :: rest) =
    if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) (digitChar (n % b) :: rest)
Tactic:
conv =>
  right; rw [Nat.todigitsCore_accumulates_suffix]
Proof state after:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
⊢ (if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n' (n / b) [] ++ digitChar (n % b) :: rest) =
    if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) [] ++ digitChar (n % b) :: rest
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
⊢ (if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n' (n / b) [] ++ digitChar (n % b) :: rest) =
    if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) [] ++ digitChar (n % b) :: rest
Tactic:
split
Proof state after:
case inl
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : n / b = 0
⊢ digitChar (n % b) :: rest = digitChar (n % b) :: rest

case inr
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ toDigitsCore b n' (n / b) [] ++ digitChar (n % b) :: rest = toDigitsCore b n (n / b) [] ++ digitChar (n % b) :: rest
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : n / b = 0
⊢ digitChar (n % b) :: rest = digitChar (n % b) :: rest
Tactic:
case inl =>
  rfl
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ toDigitsCore b n' (n / b) [] ++ digitChar (n % b) :: rest = toDigitsCore b n (n / b) [] ++ digitChar (n % b) :: rest
Tactic:
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
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : n / b = 0
⊢ digitChar (n % b) :: rest = digitChar (n % b) :: rest
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ toDigitsCore b n' (n / b) [] ++ digitChar (n % b) :: rest = toDigitsCore b n (n / b) [] ++ digitChar (n % b) :: rest
Tactic:
simp
Proof state after:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ toDigitsCore b n' (n / b) [] = toDigitsCore b n (n / b) []
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ toDigitsCore b n' (n / b) [] = toDigitsCore b n (n / b) []
Tactic:
rw [ih]
Proof state after:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ toDigitsCore b (n / b + 1) (n / b) [] = toDigitsCore b n (n / b) []

case a
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ n' < succ n'

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

case a
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ n' < succ n'

case P
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ n' ≥ n / b + 1
Tactic:
.  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]
Proof state after:
case a
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ n' < succ n'

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

case P
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ n' ≥ n / b + 1
Tactic:
. simp
Proof state after:
case P
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ n' ≥ n / b + 1
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case P
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
⊢ n' ≥ n / b + 1
Tactic:
. 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:
case false
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : (n == n / b + 1) = false
⊢ toDigitsCore b (n / b + 1) (n / b) [] = toDigitsCore b n (n / b) []
Tactic:
simp at h
Proof state after:
case false
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ toDigitsCore b (n / b + 1) (n / b) [] = toDigitsCore b n (n / b) []
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case false
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ toDigitsCore b (n / b + 1) (n / b) [] = toDigitsCore b n (n / b) []
Tactic:
rw [← Nat.toDigits, ih, ← Nat.toDigits]
Proof state after:
case false.a
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ n < succ n'

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

case false.P
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ n ≥ n / b + 1
Tactic:
. calc
    succ n' ≥  n + 1 := P
    _ > n := by simp only [gt_iff_lt, lt_add_iff_pos_right]
Proof state after:
case false.P
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ n ≥ n / b + 1
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case false.P
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ n ≥ n / b + 1
Tactic:
. 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₂
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ n + 1 > n
Tactic:
simp only [gt_iff_lt, lt_add_iff_pos_right]
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ n ≥ n / b + 1
Tactic:
simp
Proof state after:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ n / b + 1 ≤ n
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ n / b + 1 ≤ n
Tactic:
apply Nat.div_lt_self
Proof state after:
case hLtN
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ 0 < n

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

case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ 1 < b
Tactic:
. apply Nat.pos_of_ne_zero; intro h; simp only [gt_iff_lt, h, Nat.zero_div, not_true] at *
Proof state after:
case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ 1 < b
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case hLtK
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
⊢ 1 < b
Tactic:
. exact Q
Proof state after:
no goals
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case false.P.inl
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
h₂ : n / b + 1 ≤ n
h₄ : n / b + 1 = n
⊢ n / b + 1 ≤ n
Tactic:
exfalso
Proof state after:
case false.P.inl.h
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
h₂ : n / b + 1 ≤ n
h₄ : n / b + 1 = n
⊢ False
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case false.P.inl.h
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
h₂ : n / b + 1 ≤ n
h₄ : n / b + 1 = n
⊢ False
Tactic:
apply h
Proof state after:
case false.P.inl.h
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
h₂ : n / b + 1 ≤ n
h₄ : n / b + 1 = n
⊢ n = n / b + 1
Theorem: Nat.toDigitsCore_fuel_irrelevant
Proof state before:
case false.P.inl.h
b : ℕ
Q : b > 1
n : ℕ
rest : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
n' : ℕ
ih :
  ∀ (m : ℕ),
    m < succ n' → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
P : succ n' ≥ n + 1
h✝ : ¬n / b = 0
h : ¬n = n / b + 1
h₂ : n / b + 1 ≤ n
h₄ : n / b + 1 = n
⊢ n = n / b + 1
Tactic:
simp only [h₄]
Proof state after:
no goals