Theorem: List.get_zero_cons_tail (One.lean)

State before:
α : Type u_1
l : List α
h : 0 < length l
⊢ get l { val := 0, isLt := h } :: tail l = l
Tactic:
cases l with
| nil => simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, length_nil, lt_self_iff_false] at h
| cons => simp only [get, tail_cons]
State after:
no goals

State before:
case nil
α : Type u_1
h : 0 < length []
⊢ get [] { val := 0, isLt := h } :: tail [] = []
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, length_nil, lt_self_iff_false] at h
State after:
no goals

State before:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
h : 0 < length (head✝ :: tail✝)
⊢ get (head✝ :: tail✝) { val := 0, isLt := h } :: tail (head✝ :: tail✝) = head✝ :: tail✝
Tactic:
simp only [get, tail_cons]
State after:
no goals