Sequence with case split

[dranov]

In Coq, I can write something like:

Lemma lastP s : last_spec s.
Proof. case: s => [|x s]; [left | rewrite lastI; right]. Qed.

Is there something similar in Ssrlean?

Currently I do the following, which is a bit verbose:

theorem lastP (s : Seq α) : last_spec s := by
  scase: s => [|x s]
  { left }
  { srw lastI; right }

[volodeyka]

I've never been into the [ .. | .. | ...] syntax for tactics. It actually comes from vanilla Coq, and (I suggest) not idiomatic in Lean. Maybe you can try something like:

theorem lastP (s : Seq α) : last_spec s := by
  scase: s => [|x s]; { left }; srw lastI; right