Theorem: List.getLastD_ne_nil (One.lean)

State before:
α✝ : Type u_1
l : List α✝
a : α✝
h : l ≠ []
⊢ getLastD l a = getLast l h
Tactic:
cases l with
| nil => contradiction
| cons hd tl =>
  rw [List.getLastD_cons, List.getLast_eq_getLastD]
State after:
no goals

State before:
case nil
α✝ : Type u_1
a : α✝
h : [] ≠ []
⊢ getLastD [] a = getLast [] h
Tactic:
contradiction
State after:
no goals

State before:
case cons
α✝ : Type u_1
a hd : α✝
tl : List α✝
h : hd :: tl ≠ []
⊢ getLastD (hd :: tl) a = getLast (hd :: tl) h
Tactic:
rw [List.getLastD_cons, List.getLast_eq_getLastD]
State after:
no goals