linear_combination bug?

Stream: mathlib4

[Heather Macbeth]

I think I have found a bug in linear_combination, maybe @Mario Carneiro or @Rob Lewis will be interested. In this example linear_combination seems to act in a tactic proof using a former version of a certain hypothesis, not the hypothesis as it actually looks at the time linear_combination is used.

import Mathlib.Tactic.Polyrith

def g (a : ℤ) : ℤ := a ^ 2

example (h : g a = g b) : a ^ 4 = b ^ 4 := by
  dsimp [g] at h
  linear_combination (a ^ 2 + b ^ 2) * h -- fails

example (h : g a = g b) : a ^ 4 = b ^ 4 := by
  dsimp [g] at h
  linear_combination (norm := skip) (a ^ 2 + b ^ 2) * h
  -- gives more information: `g` has been reintroduced??

[Mario Carneiro]

mathlib4#2072, and I'm sure you can guess what the bug is