Theorem: Nat.toDigitsCore_ne_nil (One.lean)

State before:
f n b : ℕ
a : List Char
P : f > n
⊢ toDigitsCore b f n a ≠ []
Tactic:
unfold Nat.toDigitsCore
State after:
f n b : ℕ
a : List Char
P : f > n
⊢ (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)) ≠
    []

State before:
f n b : ℕ
a : List Char
P : f > n
⊢ (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)) ≠
    []
Tactic:
split
State after:
case h_1
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
P : 0 > n
⊢ a ≠ []

case h_2
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ > n
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) ≠
    []

State before:
case h_1
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
P : 0 > n
⊢ a ≠ []

case h_2
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ > n
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) ≠
    []
Tactic:
. case _ => contradiction
State after:
case h_2
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ > n
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) ≠
    []

State before:
case h_2
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ > n
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: a else toDigitsCore b fuel✝ n' (d :: a)) ≠
    []
Tactic:
. case _ _ _ _ fuel =>
  simp
  have h: ∀x, List.length (Nat.toDigitsCore b fuel (n / b) (x :: a)) ≠ 0 := by
    simp [Nat.to_digits_core_lens_eq]
  split
  case _ => simp
  case _ => 
    intro P₂
    apply h
    rw [P₂]
    simp
State after:
no goals

State before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
P : 0 > n
⊢ a ≠ []
Tactic:
contradiction
State after:
no goals

State before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then d :: a else toDigitsCore b fuel n' (d :: a)) ≠
    []
Tactic:
simp
State after:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
⊢ ¬(if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)) = []

State before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
⊢ ¬(if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)) = []
Tactic:
have h: ∀x, List.length (Nat.toDigitsCore b fuel (n / b) (x :: a)) ≠ 0 := by
  simp [Nat.to_digits_core_lens_eq]
State after:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
⊢ ¬(if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)) = []

State before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
⊢ ¬(if n / b = 0 then digitChar (n % b) :: a else toDigitsCore b fuel (n / b) (digitChar (n % b) :: a)) = []
Tactic:
split
State after:
case inl
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : n / b = 0
⊢ ¬False

case inr
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
⊢ ¬toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []

State before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : n / b = 0
⊢ ¬False
Tactic:
case _ => simp
State after:
no goals

State before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
⊢ ¬toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
Tactic:
case _ => 
  intro P₂
  apply h
  rw [P₂]
  simp
State after:
no goals

State before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
⊢ ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
Tactic:
simp [Nat.to_digits_core_lens_eq]
State after:
no goals

State before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : n / b = 0
⊢ ¬False
Tactic:
simp
State after:
no goals

State before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
⊢ ¬toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
Tactic:
intro P₂
State after:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ False

State before:
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ False
Tactic:
apply h
State after:
case a
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ List.length (toDigitsCore b fuel (n / b) (?x :: a)) = 0

case x
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ Char

State before:
case a
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ List.length (toDigitsCore b fuel (n / b) (?x :: a)) = 0

case x
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ Char
Tactic:
rw [P₂]
State after:
case a
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ List.length [] = 0

State before:
case a
n b : ℕ
a : List Char
x✝² x✝¹ : ℕ
x✝ : List Char
fuel : ℕ
P : succ fuel > n
h : ∀ (x : Char), List.length (toDigitsCore b fuel (n / b) (x :: a)) ≠ 0
h✝ : ¬n / b = 0
P₂ : toDigitsCore b fuel (n / b) (digitChar (n % b) :: a) = []
⊢ List.length [] = 0
Tactic:
simp
State after:
no goals