Theorem: Nat.toDigits_single_digit (One.lean)

State before:
b n : ℕ
P : n < b
⊢ toDigits b n = [digitChar n]
Tactic:
unfold toDigits toDigitsCore
State after:
b n : ℕ
P : n < b
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then [d] else toDigitsCore b (Nat.add n 0) n' [d]) =
    [digitChar n]

State before:
b n : ℕ
P : n < b
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then [d] else toDigitsCore b (Nat.add n 0) n' [d]) =
    [digitChar n]
Tactic:
simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero, add_eq, add_zero]
State after:
b n : ℕ
P : n < b
⊢ (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b n (n / b) [digitChar (n % b)]) = [digitChar n]

State before:
b n : ℕ
P : n < b
⊢ (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b n (n / b) [digitChar (n % b)]) = [digitChar n]
Tactic:
split
State after:
case inl
b n : ℕ
P : n < b
h✝ : n / b = 0
⊢ [digitChar (n % b)] = [digitChar n]

case inr
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ toDigitsCore b n (n / b) [digitChar (n % b)] = [digitChar n]

State before:
case inl
b n : ℕ
P : n < b
h✝ : n / b = 0
⊢ [digitChar (n % b)] = [digitChar n]

case inr
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ toDigitsCore b n (n / b) [digitChar (n % b)] = [digitChar n]
Tactic:
. next => 
  have h:n % b = n := by exact mod_eq_of_lt P
  simp only [h]
State after:
case inr
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ toDigitsCore b n (n / b) [digitChar (n % b)] = [digitChar n]

State before:
case inr
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ toDigitsCore b n (n / b) [digitChar (n % b)] = [digitChar n]
Tactic:
. next =>
  unfold toDigitsCore
  simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero]
  split
  . simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_mod]
  . split
    . next h _=> exfalso; apply h; exact div_eq_of_lt P
    . next h _=> exfalso; apply h; exact div_eq_of_lt P
State after:
no goals

State before:
b n : ℕ
P : n < b
h✝ : n / b = 0
⊢ [digitChar (n % b)] = [digitChar n]
Tactic:
have h:n % b = n := by exact mod_eq_of_lt P
State after:
b n : ℕ
P : n < b
h✝ : n / b = 0
h : n % b = n
⊢ [digitChar (n % b)] = [digitChar n]

State before:
b n : ℕ
P : n < b
h✝ : n / b = 0
h : n % b = n
⊢ [digitChar (n % b)] = [digitChar n]
Tactic:
simp only [h]
State after:
no goals

State before:
b n : ℕ
P : n < b
h✝ : n / b = 0
⊢ n % b = n
Tactic:
exact mod_eq_of_lt P
State after:
no goals

State before:
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ toDigitsCore b n (n / b) [digitChar (n % b)] = [digitChar n]
Tactic:
unfold toDigitsCore
State after:
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ (match n, n / b, [digitChar (n % b)] 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)) =
    [digitChar n]

State before:
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ (match n, n / b, [digitChar (n % b)] 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)) =
    [digitChar n]
Tactic:
simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero]
State after:
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ (match n, n / b, [digitChar (n % b)] 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)) =
    [digitChar n]

State before:
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ (match n, n / b, [digitChar (n % b)] 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)) =
    [digitChar n]
Tactic:
split
State after:
case h_1
b x✝² x✝¹ : ℕ
x✝ : List Char
P : 0 < b
h✝ : ¬0 / b = 0
⊢ [digitChar (0 % b)] = [digitChar 0]

case h_2
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h✝ : ¬succ fuel✝ / b = 0
⊢ (if succ fuel✝ / b / b = 0 then [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]
    else toDigitsCore b fuel✝ (succ fuel✝ / b / b) [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]) =
    [digitChar (succ fuel✝)]

State before:
case h_1
b x✝² x✝¹ : ℕ
x✝ : List Char
P : 0 < b
h✝ : ¬0 / b = 0
⊢ [digitChar (0 % b)] = [digitChar 0]

case h_2
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h✝ : ¬succ fuel✝ / b = 0
⊢ (if succ fuel✝ / b / b = 0 then [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]
    else toDigitsCore b fuel✝ (succ fuel✝ / b / b) [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]) =
    [digitChar (succ fuel✝)]
Tactic:
. simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_mod]
State after:
case h_2
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h✝ : ¬succ fuel✝ / b = 0
⊢ (if succ fuel✝ / b / b = 0 then [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]
    else toDigitsCore b fuel✝ (succ fuel✝ / b / b) [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]) =
    [digitChar (succ fuel✝)]

State before:
case h_2
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h✝ : ¬succ fuel✝ / b = 0
⊢ (if succ fuel✝ / b / b = 0 then [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]
    else toDigitsCore b fuel✝ (succ fuel✝ / b / b) [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]) =
    [digitChar (succ fuel✝)]
Tactic:
. split
  . next h _=> exfalso; apply h; exact div_eq_of_lt P
  . next h _=> exfalso; apply h; exact div_eq_of_lt P
State after:
no goals

State before:
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : succ fuel✝ / b / b = 0
⊢ [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)] = [digitChar (succ fuel✝)]
Tactic:
exfalso
State after:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : succ fuel✝ / b / b = 0
⊢ False

State before:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : succ fuel✝ / b / b = 0
⊢ False
Tactic:
apply h
State after:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : succ fuel✝ / b / b = 0
⊢ succ fuel✝ / b = 0

State before:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : succ fuel✝ / b / b = 0
⊢ succ fuel✝ / b = 0
Tactic:
exact div_eq_of_lt P
State after:
no goals

State before:
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : ¬succ fuel✝ / b / b = 0
⊢ toDigitsCore b fuel✝ (succ fuel✝ / b / b) [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)] =
    [digitChar (succ fuel✝)]
Tactic:
exfalso
State after:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : ¬succ fuel✝ / b / b = 0
⊢ False

State before:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : ¬succ fuel✝ / b / b = 0
⊢ False
Tactic:
apply h
State after:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : ¬succ fuel✝ / b / b = 0
⊢ succ fuel✝ / b = 0

State before:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : ¬succ fuel✝ / b / b = 0
⊢ succ fuel✝ / b = 0
Tactic:
exact div_eq_of_lt P
State after:
no goals