dot notation in a cases match

Stream: lean4

[Adam Topaz]

It seems that there is some inconsistency around naming things using the cases tactic, specifically around dot notation.
For example the following works perfectly fine

inductive thing
| a : thing
| b : thing

example (x : thing) : x = .a ∨ x = .b := by
  cases x with
  | a => exact Or.inl rfl
  | b => exact Or.inr rfl

but the following two variants give errors

-- Error
example (x : thing) : x = .a ∨ x = .b := by
  cases x with
  | thing.a => sorry -- invalid alternative name 'thing.a'
  | thing.b => sorry

-- Error
example (x : thing) : x = .a ∨ x = .b := by
  cases x with
  | .a => sorry -- expected '_' or identifier
  | .b => sorry

Of course, using a plain match works just as expected:

-- Fine
example (x : thing) : x = .a ∨ x = .b :=
match x with
| .a => sorry
| .b => sorry

Is this intended behavior? Maybe I'm the only one bothered by this :)