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

State before:
α : Type u_1
⊢ ∀ (xs : List α) (n : ℕ), 0 < n ∧ n ≤ length xs → take n xs ≠ []
Tactic:
intro xs n range h
State after:
α : Type u_1
xs : List α
n : ℕ
range : 0 < n ∧ n ≤ length xs
h : take n xs = []
⊢ False

State before:
α : Type u_1
xs : List α
n : ℕ
range : 0 < n ∧ n ≤ length xs
h : take n xs = []
⊢ False
Tactic:
cases range with
| intro notzero max =>
  cases n with
  | zero =>
    contradiction
  | succ n =>
    cases xs with
    | nil =>
      contradiction
    | cons x xs =>
      simp only [succ_pos', take] at *
State after:
no goals

State before:
case intro
α : Type u_1
xs : List α
n : ℕ
h : take n xs = []
notzero : 0 < n
max : n ≤ length xs
⊢ False
Tactic:
cases n with
| zero =>
  contradiction
| succ n =>
  cases xs with
  | nil =>
    contradiction
  | cons x xs =>
    simp only [succ_pos', take] at *
State after:
no goals

State before:
case intro.zero
α : Type u_1
xs : List α
h : take zero xs = []
notzero : 0 < zero
max : zero ≤ length xs
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case intro.succ
α : Type u_1
xs : List α
n : ℕ
h : take (succ n) xs = []
notzero : 0 < succ n
max : succ n ≤ length xs
⊢ False
Tactic:
cases xs with
| nil =>
  contradiction
| cons x xs =>
  simp only [succ_pos', take] at *
State after:
no goals

State before:
case intro.succ.nil
α : Type u_1
n : ℕ
notzero : 0 < succ n
h : take (succ n) [] = []
max : succ n ≤ length []
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case intro.succ.cons
α : Type u_1
n : ℕ
notzero : 0 < succ n
x : α
xs : List α
h : take (succ n) (x :: xs) = []
max : succ n ≤ length (x :: xs)
⊢ False
Tactic:
simp only [succ_pos', take] at *
State after:
no goals