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

[dwrensha]

(Originally noted in #27562 (comment)).

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