Theorem: Int.reprΔ_ne_nil (One.lean)

State before:
i : ℤ
⊢ reprΔ i ≠ []
Tactic:
unfold Int.reprΔ
State after:
i : ℤ
⊢ (match i with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)) ≠
    []

State before:
i : ℤ
⊢ (match i with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)) ≠
    []
Tactic:
cases i with
| ofNat m => simp only; apply Nat.toDigits_ne_nil
| negSucc m => simp only [List.singleton_append, ne_eq, not_false_iff]
State after:
no goals

State before:
case ofNat
m : ℕ
⊢ (match ofNat m with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)) ≠
    []
Tactic:
simp only
State after:
case ofNat
m : ℕ
⊢ Nat.toDigits 10 m ≠ []

State before:
case ofNat
m : ℕ
⊢ Nat.toDigits 10 m ≠ []
Tactic:
apply Nat.toDigits_ne_nil
State after:
no goals

State before:
case negSucc
m : ℕ
⊢ (match -[m+1] with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)) ≠
    []
Tactic:
simp only [List.singleton_append, ne_eq, not_false_iff]
State after:
no goals