Theorem: Nat.toDigitsCore_fuel_irrelevant (One.lean)

State before:
f n b : ℕ
rest : List Char
P : f ≥ n + 1
Q : b > 1
⊢ toDigitsCore b f n rest = toDigitsCore b (n + 1) n rest
Tactic:
induction f using Nat.strong_induction_on generalizing rest n
State after:
case h
b : ℕ
Q : b > 1
n✝ : ℕ
a✝ :
  ∀ (m : ℕ), m < n✝ → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : n✝ ≥ n + 1
⊢ toDigitsCore b n✝ n rest = toDigitsCore b (n + 1) n rest

State before:
b : ℕ
Q : b > 1
f : ℕ
ih :
  ∀ (m : ℕ), m < f → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : f ≥ n + 1
⊢ toDigitsCore b f n rest = toDigitsCore b (n + 1) n rest
Tactic:
case h f ih =>
  unfold toDigitsCore
  simp
  split
  case h_1 =>
    simp at P
  case h_2 n' =>
    conv =>
      left; rw [Nat.todigitsCore_accumulates_suffix]
    conv =>
      right; rw [Nat.todigitsCore_accumulates_suffix]
    split
    case inl =>
      rfl
    case inr =>
      simp
      rw [ih]
      .  cases h: n == (n / b) + 1 with
          | false => 
            simp at h
            rw [← Nat.toDigits, ih, ← Nat.toDigits]
            . calc
                succ n' ≥  n + 1 := P
                _ > n := by simp only [gt_iff_lt, lt_add_iff_pos_right]
            . simp [h]
              have h₂: n ≥  n / b + 1 := by 
                simp
                apply Nat.div_lt_self
                . apply Nat.pos_of_ne_zero; intro h; simp only [gt_iff_lt, h, Nat.zero_div, not_true] at *
                . exact Q
              simp [ge_iff_le] at h₂
              have h₃:= Nat.eq_or_lt_of_le h₂
              cases h₃ with
              | inl h₄ => exfalso; apply h; simp only [h₄]
              | inr h₄ => exact h₂
          | true => 
            simp at h
            rw [← h]
      . simp
      . simp [Nat.succ_eq_add_one] at P 
        calc
          n' ≥  n        := P
          n ≥ n / b + 1 := by simp only [add_lt_add_iff_right]; apply Nat.div_lt_self; apply Nat.pos_of_ne_zero; intro h; simp only [gt_iff_lt, h, Nat.zero_div, not_true] at *; apply Q
State after:
no goals

State before:
b : ℕ
Q : b > 1
f : ℕ
ih :
  ∀ (m : ℕ), m < f → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : f ≥ n + 1
⊢ toDigitsCore b f n rest = toDigitsCore b (n + 1) n rest
Tactic:
unfold toDigitsCore
State after:
b : ℕ
Q : b > 1
f : ℕ
ih :
  ∀ (m : ℕ), m < f → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : f ≥ n + 1
⊢ (match f, n, rest with
    | 0, x, ds => ds
    | succ fuel, n, ds =>
      let d := digitChar (n % b);
      let n' := n / b;
      if n' = 0 then d :: ds else toDigitsCore b fuel n' (d :: ds)) =
    let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: rest else toDigitsCore b (Nat.add n 0) n' (d :: rest)

State before:
b : ℕ
Q : b > 1
f : ℕ
ih :
  ∀ (m : ℕ), m < f → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : f ≥ n + 1
⊢ (match f, n, rest with
    | 0, x, ds => ds
    | succ fuel, n, ds =>
      let d := digitChar (n % b);
      let n' := n / b;
      if n' = 0 then d :: ds else toDigitsCore b fuel n' (d :: ds)) =
    let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: rest else toDigitsCore b (Nat.add n 0) n' (d :: rest)
Tactic:
simp
State after:
b : ℕ
Q : b > 1
f : ℕ
ih :
  ∀ (m : ℕ), m < f → ∀ {n : ℕ} {rest : List Char}, m ≥ n + 1 → toDigitsCore b m n rest = toDigitsCore b (n + 1) n rest
n : ℕ
rest : List Char
P : f ≥ n + 1
⊢ (match f, n, rest with
    | 0, x, ds => ds
    | succ fuel, n, ds =>
      if n / b = 0 then digitChar (n % b) :: ds else toDigitsCore b fuel (n / b) (digitChar (n % b) :: ds)) =
    if n / b = 0 then digitChar (n % b) :: rest else toDigitsCore b n (n / b) (digitChar (n % b) :: rest)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

State before:
case false.P.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
h : ¬n = n / b + 1
h₂ : n / b + 1 ≤ n
h₄ : n / b + 1 < n
⊢ n / b + 1 ≤ n
Tactic:
exact h₂
State after:
no goals

State before:
case true
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) = true
⊢ toDigitsCore b (n / b + 1) (n / b) [] = toDigitsCore b n (n / b) []
Tactic:
simp at h
State after:
case true
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) []

State before:
case true
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 [← h]
State after:
no goals

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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ n ≥ n / b + 1
Tactic:
apply Nat.div_lt_self
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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b

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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Tactic:
apply Nat.pos_of_ne_zero
State after:
case hLtN.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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ n ≠ 0

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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b

State before:
case hLtN.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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ n ≠ 0

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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Tactic:
intro h
State after:
case hLtN.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
h✝ : ¬n / b = 0
P : n ≤ n'
h : n = 0
⊢ False

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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b

State before:
case hLtN.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
h✝ : ¬n / b = 0
P : n ≤ n'
h : n = 0
⊢ False

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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Tactic:
simp only [gt_iff_lt, h, Nat.zero_div, not_true] at *
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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b

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
h✝ : ¬n / b = 0
P : n ≤ n'
⊢ 1 < b
Tactic:
apply Q
State after:
no goals