over-zealous `cases` code action

[kbuzzard]

This code

import Mathlib.Tactic

inductive Relation (n : ℕ) : ℕ → ℕ → Prop

example {x y z} (r : Relation x y z) : true := by
  cases r

followed by clicking the lightbulb and selecting "Generate an explicit pattern match for rcases" gives me the exciting output

example {x y z} (r : Relation x y z) : true := by
  cases r with
  | n => sorry
  | a._@.scratch._hyg.6 => sorry
  | a._@.scratch._hyg.10 => sorry

Examples of this showing up in the wild: here, here (including MWE), here.