Theorem: List.getSnoc?_eq_none (LeanColls/Data/List.lean)

State before:
α : Type u_1
c : List α
⊢ c.getSnoc? = none ↔ c = []
Tactic:
induction c <;> simp_all [getSnoc?]
State after:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.getSnoc? = none ↔ tail✝ = []
⊢ ¬(match tail✝.getSnoc? with
      | none => some ([], head✝)
      | some (xs', x') => some (head✝ :: xs', x')) =
      none

State before:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.getSnoc? = none ↔ tail✝ = []
⊢ ¬(match tail✝.getSnoc? with
      | none => some ([], head✝)
      | some (xs', x') => some (head✝ :: xs', x')) =
      none
Tactic:
intro h
State after:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.getSnoc? = none ↔ tail✝ = []
h :
  (match tail✝.getSnoc? with
    | none => some ([], head✝)
    | some (xs', x') => some (head✝ :: xs', x')) =
    none
⊢ False

State before:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.getSnoc? = none ↔ tail✝ = []
h :
  (match tail✝.getSnoc? with
    | none => some ([], head✝)
    | some (xs', x') => some (head✝ :: xs', x')) =
    none
⊢ False
Tactic:
split at h <;> simp_all
State after:
no goals