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

State before:
α : Type u_1
n : ℕ
xs : List α
⊢ length xs ≤ n → drop n xs = []
Tactic:
revert xs
State after:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), length xs ≤ n → drop n xs = []

State before:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), length xs ≤ n → drop n xs = []
Tactic:
induction n with
| zero =>
  intro xs
  intro h
  have empty_list := list_length_zero_or_smaller_is_empty xs h
  rw [empty_list]
  rw [drop]
| succ n ih =>
  intro xs
  cases xs with
  | nil =>
    rw [length]
    intro _
    rw [drop]
  | cons x xs =>
    rw [length]
    intro h
    rw [drop]
    rw [nat_succ_le_succ_iff] at h
    exact ih xs h
State after:
no goals

State before:
case zero
α : Type u_1
⊢ ∀ (xs : List α), length xs ≤ zero → drop zero xs = []
Tactic:
intro xs
State after:
case zero
α : Type u_1
xs : List α
⊢ length xs ≤ zero → drop zero xs = []

State before:
case zero
α : Type u_1
xs : List α
⊢ length xs ≤ zero → drop zero xs = []
Tactic:
intro h
State after:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ drop zero xs = []

State before:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ drop zero xs = []
Tactic:
have empty_list := list_length_zero_or_smaller_is_empty xs h
State after:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
empty_list : xs = []
⊢ drop zero xs = []

State before:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
empty_list : xs = []
⊢ drop zero xs = []
Tactic:
rw [empty_list]
State after:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
empty_list : xs = []
⊢ drop zero [] = []

State before:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
empty_list : xs = []
⊢ drop zero [] = []
Tactic:
rw [drop]
State after:
no goals

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
⊢ ∀ (xs : List α), length xs ≤ succ n → drop (succ n) xs = []
Tactic:
intro xs
State after:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
xs : List α
⊢ length xs ≤ succ n → drop (succ n) xs = []

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
xs : List α
⊢ length xs ≤ succ n → drop (succ n) xs = []
Tactic:
cases xs with
| nil =>
  rw [length]
  intro _
  rw [drop]
| cons x xs =>
  rw [length]
  intro h
  rw [drop]
  rw [nat_succ_le_succ_iff] at h
  exact ih xs h
State after:
no goals

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
⊢ length [] ≤ succ n → drop (succ n) [] = []
Tactic:
rw [length]
State after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
⊢ 0 ≤ succ n → drop (succ n) [] = []

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
⊢ 0 ≤ succ n → drop (succ n) [] = []
Tactic:
intro _
State after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
a✝ : 0 ≤ succ n
⊢ drop (succ n) [] = []

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
a✝ : 0 ≤ succ n
⊢ drop (succ n) [] = []
Tactic:
rw [drop]
State after:
no goals

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
⊢ length (x :: xs) ≤ succ n → drop (succ n) (x :: xs) = []
Tactic:
rw [length]
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
⊢ length xs + 1 ≤ succ n → drop (succ n) (x :: xs) = []

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
⊢ length xs + 1 ≤ succ n → drop (succ n) (x :: xs) = []
Tactic:
intro h
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs + 1 ≤ succ n
⊢ drop (succ n) (x :: xs) = []

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs + 1 ≤ succ n
⊢ drop (succ n) (x :: xs) = []
Tactic:
rw [drop]
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs + 1 ≤ succ n
⊢ drop n xs = []

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs + 1 ≤ succ n
⊢ drop n xs = []
Tactic:
rw [nat_succ_le_succ_iff] at h
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs ≤ n
⊢ drop n xs = []

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs ≤ n
⊢ drop n xs = []
Tactic:
exact ih xs h
State after:
no goals