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

State before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) ≤ n
Tactic:
revert n
State after:
α : Type u_1
xs : List α
⊢ ∀ (n : ℕ), length (take n xs) ≤ n

State before:
α : Type u_1
xs : List α
⊢ ∀ (n : ℕ), length (take n xs) ≤ n
Tactic:
induction xs with
| nil =>
  intro n
  rw [list_take_nil]
  simp
| cons head tail ih =>
  intro n
  cases n with
  | zero  =>
    rw [take]
    simp only [length_nil, zero_eq, le_refl]
  | succ k =>
    rw [take]
    rw [length]
    apply Nat.succ_le_succ
    apply (ih k)
State after:
no goals

State before:
case nil
α : Type u_1
⊢ ∀ (n : ℕ), length (take n []) ≤ n
Tactic:
intro n
State after:
case nil
α : Type u_1
n : ℕ
⊢ length (take n []) ≤ n

State before:
case nil
α : Type u_1
n : ℕ
⊢ length (take n []) ≤ n
Tactic:
rw [list_take_nil]
State after:
case nil
α : Type u_1
n : ℕ
⊢ length [] ≤ n

State before:
case nil
α : Type u_1
n : ℕ
⊢ length [] ≤ n
Tactic:
simp
State after:
no goals

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
⊢ ∀ (n : ℕ), length (take n (head :: tail)) ≤ n
Tactic:
intro n
State after:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
n : ℕ
⊢ length (take n (head :: tail)) ≤ n

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
n : ℕ
⊢ length (take n (head :: tail)) ≤ n
Tactic:
cases n with
| zero  =>
  rw [take]
  simp only [length_nil, zero_eq, le_refl]
| succ k =>
  rw [take]
  rw [length]
  apply Nat.succ_le_succ
  apply (ih k)
State after:
no goals

State before:
case cons.zero
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
⊢ length (take zero (head :: tail)) ≤ zero
Tactic:
rw [take]
State after:
case cons.zero
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
⊢ length [] ≤ zero

State before:
case cons.zero
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
⊢ length [] ≤ zero
Tactic:
simp only [length_nil, zero_eq, le_refl]
State after:
no goals

State before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (take (succ k) (head :: tail)) ≤ succ k
Tactic:
rw [take]
State after:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (head :: take k tail) ≤ succ k

State before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (head :: take k tail) ≤ succ k
Tactic:
rw [length]
State after:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (take k tail) + 1 ≤ succ k

State before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (take k tail) + 1 ≤ succ k
Tactic:
apply Nat.succ_le_succ
State after:
case cons.succ.a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (take k tail) ≤ k

State before:
case cons.succ.a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (take k tail) ≤ k
Tactic:
apply (ih k)
State after:
no goals