Obtain misses `toLex`

Stream: mathlib4

[Daniel Weber]

I'm trying to use obtain/rcases for a value of Lex, and it doesn't work properly. Is this a bug? Am I doing something wrong?
Either it doesn't do anything:

import Mathlib.Tactic

example {α : Type*} (b : α ⊕ₗ α) [LinearOrder α] (h : ∃ a : α ⊕ₗ α, a < b) : False := by
  obtain ⟨a, ha⟩ := h
  rcases a with c
  /-
  α: Type u_1
  b: Lex (α ⊕ α)
  inst✝: LinearOrder α
  a: Lex (α ⊕ α)
  ha: a < b
  ⊢ False
  -/
  trace_state
  done

Or it eliminates, but without toLex:

import Mathlib.Tactic

example {α : Type*} (b : α ⊕ₗ α) [LinearOrder α] (h : ∃ a : α ⊕ₗ α, a < b) : False := by
  obtain ⟨⟨a⟩ | ⟨a⟩, ha⟩ := h
  /-
  α: Type u_1
  b: Lex (α ⊕ α)
  inst✝: LinearOrder α
  a: α
  ha: Sum.inl a < b
  ⊢ False


  α: Type u_1
  b: Lex (α ⊕ α)
  inst✝: LinearOrder α
  a: α
  ha: Sum.inr a < b
  ⊢ False
  -/
  trace_state
  done

for comparison, here is what I'm expecting:

example {α : Type*} (b : α ⊕ₗ α) [LinearOrder α] (h : ∃ a : α ⊕ₗ α, a < b) : False := by
  obtain ⟨a, ha⟩ := h
  cases' a with a
  rcases a with a | a
  /-
  α: Type u_1
  b: Lex (α ⊕ α)
  inst✝: LinearOrder α
  a: α
  ha: toLex (Sum.inl a) < b
  ⊢ False


  α: Type u_1
  b: Lex (α ⊕ α)
  inst✝: LinearOrder α
  a: α
  ha: toLex (Sum.inr a) < b
  ⊢ False
  -/
  trace_state
  done

[Eric Wieser]

I think this will work with let, as long as you write the .toLex explicitly

[Daniel Weber]

How? let ⟨toLex a, ha⟩ := h doesn't work

[Eric Wieser]

Does it work with .toLex?

[Eric Wieser]

I guess it's an equiv so probably not

[Daniel Weber]

Nope

[Eric Wieser]

What's the error?

[Daniel Weber]

invalid dotted identifier notation, unknown identifier `Sum.toLex` from expected type
  Lex (α ⊕ α)

[Eric Wieser]

And without the .?

[Eric Wieser]

Huh, "too many arguments"

[Yury G. Kudryashov]

Lex is a type synonym, so rcases doesn't know that it needs to unfold it.

[Yury G. Kudryashov]

As a workaround, you can rcases toLex.surjective a

[Yury G. Kudryashov]

We can also try to add a custom cases eliminator, but I don't know which tactics will take it into account with our current setup.

[Eric Wieser]

Yury G. Kudryashov said:

We can also try to add a custom cases eliminator, but I don't know which tactics will take it into account with our current setup.

rcases doesn't pay attention to cases_eliminator

[Eric Paul]

I've had many similar such issues with toLex.

Here's something useful from when I asked something similar from @Kyle Miller

To quote it:

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

I've had other issues with Lex in these other threads in case you're curious:

• match does strange things
• generally fighting with it

[Eric Wieser]

The custom eliminator feels like overkill when you can just write

cases' a with a; obtain a | a := a

which is also shorter

[Eric Wieser]

The rule is just "obtain/rcases/match make a mess in places that induction and cases do not"

[Ruben Van de Velde]

One more point in favour of a hypothetical unified tactic :innocent: