mathlib3

6f9edf5b - fix(tactic/positivity + test): instantiate meta-variables and add a test (#16647)

fix(tactic/positivity + test): instantiate meta-variables and add a test (#16647) Fix an issue with `positivity` reported by @YaelDillies [here](https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/New.20tactic.3A.20.60positivity.60/near/300639970). For the fix, it seems that instantiating meta-variables is enough.