Theorem: list_length_gt_zero (Katydid/Std/Lists.lean)

State before:
α : Type u_1
⊢ ∀ (xs : List α), xs ≠ [] → 0 < length xs
Tactic:
intro xs
State after:
α : Type u_1
xs : List α
⊢ xs ≠ [] → 0 < length xs

State before:
α : Type u_1
xs : List α
⊢ xs ≠ [] → 0 < length xs
Tactic:
cases xs with
| nil =>
  intro h
  contradiction
| cons x xs =>
  intro _
  rw [length]
  apply Nat.zero_lt_succ
State after:
no goals

State before:
case nil
α : Type u_1
⊢ [] ≠ [] → 0 < length []
Tactic:
intro h
State after:
case nil
α : Type u_1
h : [] ≠ []
⊢ 0 < length []

State before:
case nil
α : Type u_1
h : [] ≠ []
⊢ 0 < length []
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
x : α
xs : List α
⊢ x :: xs ≠ [] → 0 < length (x :: xs)
Tactic:
intro _
State after:
case cons
α : Type u_1
x : α
xs : List α
a✝ : x :: xs ≠ []
⊢ 0 < length (x :: xs)

State before:
case cons
α : Type u_1
x : α
xs : List α
a✝ : x :: xs ≠ []
⊢ 0 < length (x :: xs)
Tactic:
rw [length]
State after:
case cons
α : Type u_1
x : α
xs : List α
a✝ : x :: xs ≠ []
⊢ 0 < length xs + 1

State before:
case cons
α : Type u_1
x : α
xs : List α
a✝ : x :: xs ≠ []
⊢ 0 < length xs + 1
Tactic:
apply Nat.zero_lt_succ
State after:
no goals