Theorem: List.lastN_eq_tail (One.lean)

State before:
α : Type u_1
l : List α
⊢ lastN (length l - 1) l = tail l
Tactic:
unfold List.lastN
State after:
α : Type u_1
l : List α
⊢ drop (length l - (length l - 1)) l = tail l

State before:
α : Type u_1
l : List α
⊢ drop (length l - (length l - 1)) l = tail l
Tactic:
rw [Nat.sub_self_sub_eq_min]
State after:
α : Type u_1
l : List α
⊢ drop (Nat.min (length l) 1) l = tail l

State before:
α : Type u_1
l : List α
⊢ drop (Nat.min (length l) 1) l = tail l
Tactic:
cases l with
| nil => simp only [drop, tail_nil]
| cons hd tl => 
  have h: Nat.succ (List.length tl) ≥ 1 := by 
    apply Nat.succ_le_succ
    apply Nat.zero_le
  simp only [length_cons, Nat.min_eq_right h, ge_iff_le, drop, tail_cons]
State after:
no goals

State before:
case nil
α : Type u_1
⊢ drop (Nat.min (length []) 1) [] = tail []
Tactic:
simp only [drop, tail_nil]
State after:
no goals

State before:
case cons
α : Type u_1
hd : α
tl : List α
⊢ drop (Nat.min (length (hd :: tl)) 1) (hd :: tl) = tail (hd :: tl)
Tactic:
have h: Nat.succ (List.length tl) ≥ 1 := by 
  apply Nat.succ_le_succ
  apply Nat.zero_le
State after:
case cons
α : Type u_1
hd : α
tl : List α
h : Nat.succ (length tl) ≥ 1
⊢ drop (Nat.min (length (hd :: tl)) 1) (hd :: tl) = tail (hd :: tl)

State before:
case cons
α : Type u_1
hd : α
tl : List α
h : Nat.succ (length tl) ≥ 1
⊢ drop (Nat.min (length (hd :: tl)) 1) (hd :: tl) = tail (hd :: tl)
Tactic:
simp only [length_cons, Nat.min_eq_right h, ge_iff_le, drop, tail_cons]
State after:
no goals

State before:
α : Type u_1
hd : α
tl : List α
⊢ Nat.succ (length tl) ≥ 1
Tactic:
apply Nat.succ_le_succ
State after:
case a
α : Type u_1
hd : α
tl : List α
⊢ 0 ≤ length tl

State before:
case a
α : Type u_1
hd : α
tl : List α
⊢ 0 ≤ length tl
Tactic:
apply Nat.zero_le
State after:
no goals