mathlib

d3b54a9f - fix(tactic/interval_cases): instantiate metavars (#19232)

fix(tactic/interval_cases): instantiate metavars (#19232) The test included in this commit fails without this change. This does not need forward-porting, the test already passes in Lean 4.