Combining `intro` and `cases`

Stream: general

[Mai]

Is there a way to combine the intro and cases tactics? for example, here:

inductive Any
opaque Any.level : Any -> Nat := nofun

structure Ctx (level : Nat) where
  vars : List Any
  var_level_le_level : ∀ v ∈ vars, v.level <= level

def Ctx.with (Γ : Ctx level) (var : Any) {var_level : var.level = level + 1} : Ctx (level + 1) :=
  { Γ with
    vars := var :: Γ.vars
    var_level_le_level v := by
      intro hv
      cases hv
      case head => simp [var_level]
      case tail mem =>
        apply Nat.le_add_right_of_le
        exact Γ.var_level_le_level v mem }

[Damiano Testa]

You can probably use the rintro tactic and then do the desctructuring there.

[Robin Arnez]

That is,

inductive Any
opaque Any.level : Any -> Nat := nofun

structure Ctx (level : Nat) where
  vars : List Any
  var_level_le_level : ∀ v ∈ vars, v.level <= level

def Ctx.with (Γ : Ctx level) (var : Any) {var_level : var.level = level + 1} : Ctx (level + 1) :=
  { Γ with
    vars := var :: Γ.vars
    var_level_le_level v := by
      rintro (_ | ⟨_, mem⟩)
      · simp [var_level]
      · apply Nat.le_add_right_of_le
        exact Γ.var_level_le_level v mem }

[Mai]

That's pretty neat. what do the underscores represent?

[Robin Arnez]

Placeholders? Just like in match

[Mai]

@Robin Arnez I mean, they aren't present in my cases version. What information do they represent

[Robin Arnez]

Well the second underscore is basically the same as in

cases  hv
case head => ...
case tail _ mem => ...

i.e. don't assign a variable name. The first underscore here is a placeholder for the constructor application of List.Mem.head, which doesn't bind any variables, so you could also write ⟨⟩ instead of the first _.