Modify how rcases matches

Stream: mathlib4

[Eric Paul]

Notice how the goals are different in test vs test2. I would like to be able to use rcases but get the same goals as when I used match. (also the weird symbol should be subscript l)

import Mathlib

variable (α : Type*) (β : Type*) [LinearOrder α] [LinearOrder β]

theorem test (a : α ⊕ₗ β) : a = a := by
  rcases a with a | a
  /-
  ⊢ Sum.inl a = Sum.inl a
  ⊢ Sum.inr a = Sum.inr a
  -/
  sorry

theorem test2 (a : α ⊕ₗ β) : a = a := by
  match a with
  | Sum.inlₗ a =>
  /-
  ⊢ Sum.inlₗ a = Sum.inlₗ a
  -/
  sorry
  | Sum.inrₗ a =>
  /-
  ⊢ Sum.inrₗ a = Sum.inrₗ a
  -/
  sorry

[Kyle Miller]

I don't think that's possible, but at least you can use cases/cases' with a using clause.

def Lex.sumCasesOn.{u, v, w} {α : Type u} {β : Type v}
    {motive : α ⊕ₗ β → Sort w}
    (t : α ⊕ₗ β)
    (inlₗ : (val : α) → motive (Sum.inlₗ val))
    (inrₗ : (val : β) → motive (Sum.inrₗ val)) : motive t :=
  Sum.casesOn t inlₗ inrₗ

theorem test (a : α ⊕ₗ β) : a = a := by
  cases' a using Lex.sumCasesOn with a a
  /-
  ⊢ Sum.inlₗ a = Sum.inlₗ a
  ⊢ Sum.inrₗ a = Sum.inrₗ a
  -/
  sorry

[Eric Paul]

I didn't know about that, thank you!