rcases?

Stream: std4

[Scott Morrison]

Could we have rcases? again? I found it very helpful navigating rcases.

[Scott Morrison]

My current pain point is just translating

import tactic.rcases

example {α : Type} {x a : α} {L : list α} (h : x ∈ a :: L) : x = a ∨ x ∈ L :=
begin
  rcases h with rfl | m,
  { left, refl, },
  { right, exact m, },
end

into Lean 4... I know the definition of List.Mem is new and different, but surely I should be able to use rcases somehow? I can't find any pattern that works:

import Std.Tactic.RCases
import Mathlib.Tactic.LeftRight

example (h : x ∈ a :: L) : x = a ∨ x ∈ L := by
  rcases h with _ | m    -- not this!
  · left
    rfl
  · right
    exact m

[Kevin Buzzard]

What happens if you just do cases' h, then edit to cases' h with <stuff>, then cases' <whatever just appeared> etc etc

[Mario Carneiro]

rcases h with _ | ⟨_, m⟩