regression: if `norm_num at h1` closes a goal then `norm_num at h1 h2` fails

(Originally noted in https://github.com/leanprover-community/mathlib4/pull/27562#issuecomment-3206051728).

The following proofs worked before #27562 and are broken after it:

import Mathlib.Tactic

example (h : 0 = 1) (h2 : 0 = 2) : False := by
  norm_num at h h2 -- error: No goals to be solved

-- slightly more realistic example
example {x : Nat} (hx : x < 2) (h : x = 1) (h2 : x = 2) : False := by
  interval_cases x <;> norm_num at h h2 -- error: No goals to be solved

It seems that if norm_num at h succeeds in closing the proof, then norm_num at h h2 is now an error.

I expect norm_num at to work the same as simp at. The following continues to work without error:

import Mathlib.Tactic

example (h : 0 = 1) (h2 : 0 = 2) : False := by
  simp at h h2

-- slightly more realistic example
example {x : Nat} (hx : x < 2) (h : x = 1) (h2 : x = 2) : False := by
  interval_cases x <;> simp at h h2

Start by reproducing the two examples after importing Mathlib.Tactic, comparing norm_num at h h2 with the working simp at h h2 behavior. Trace the norm_num at handling for multiple hypotheses, especially when processing h closes the goal; done means both examples succeed without a “No goals to be solved” error.