Naming the implicit assumption of an `@`-pattern

Stream: lean4

[Hirotaka Sato]

I don't know how to name the implicit assumption introduced by an @-pattern

def atPatternExample (list : List Nat) : Nat :=
  match list with
  | [] => sorry
  | α@(A :: γ) =>
    /-
      Here, I want to also have `h : α = A :: γ` in the assumption.
      Infoview claims `h✝ : α = A :: γ` with this at-pattern,
      but I don't know how to name it.
    -/
    sorry

[Hirotaka Sato]

I understand that the following workaround works, but it's a little too verbose and tedious to use in the true proof that I am currently writing

def atPatternExample (list : List Nat) : Nat :=
  match list with
  | [] => sorry
  | α@(A :: γ) =>
    have h : α = A :: γ := by assumption
    /-
      Here, I want to also have `h : α = A :: γ` in the assumption.
      Infoview claims `h✝ : α = A :: γ` with this at-pattern,
      but I don't know how to name it.
    -/
    sorry

[Robin Arnez]

The hover on the syntax should tell you everything:

x@e or x@h:e matches the pattern e and binds its value to the identifier x. If present, the identifier h is bound to a proof of x = e.

In other words α@h:(A :: γ)