unknown free variable in norm_num

Stream: mathlib4

[Eric Wieser]

The combination of replace (or symm at) and norm_num seems to cause a bizarre error

import Mathlib

example (a b : ℕ) (h : a * b = 1) :  a * b = 1 := by
  replace h := h.symm -- needs this line to fail
  norm_num [*] at * -- unknown free variable '_uniq.140'

[Eric Rodriguez]

@Thomas Murrills, does your fix fix this?