Confusing "cases" behaviour

Stream: mathlib4

[Heather Macbeth]

Teaching today, I noticed that if you run cases or one of its derivatives like obtain on a nonexistent hypothesis you get two different errors: first

unknown identifier

but also

tactic 'induction' failed, major premise type is not an inductive type

from Lean replacing the nonexistent hypothesis by a metavariable and then trying to split that metavariable.

example {a : Int} (H : a = 4 ∨ a = 6) : ∃ k : Int, a = 2 * a := by
  cases h

This is particularly confusing for the obtain tactic because there, because of the inverted syntax, the more useful "unknown identifier" hypothesis comes later where it is easy for a newbie to overlook.

import Std.Tactic.RCases

example {a : Int} (H : a = 4 ∨ a = 6) : ∃ k : Int, a = 2 * a := by
  obtain h1 | h2 := h

Would it be possible to change cases and its derivatives to fail fully on a metavariable?