fix(tactic/positivity + test): instantiate meta-variables and add a t…

…est (#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.

src/tactic/positivity.lean

@@ -179,7 +179,7 @@ example {b : ℤ} : 0 ≤ max (-3) (b ^ 2) := by positivity
 ```
 -/
 meta def positivity : tactic unit := focus1 $ do
-  t ← target,
+  t ← target >>= instantiate_mvars,
   (rel_desired, a) ← match t with
   | `(0 ≤ %%e₂) := pure (ff, e₂)
   | `(%%e₂ ≥ 0) := pure (ff, e₂)

test/positivity.lean

@@ -14,6 +14,15 @@ import tactic.positivity
 This tactic proves goals of the form `0 ≤ a` and `0 < a`.
 -/
 
+/-  Test for instantiating meta-variables.  Reported on
+https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/New.20tactic.3A.20.60positivity.60/near/300639970
+-/
+example : 0 ≤ 0 :=
+begin
+  apply le_trans _ le_rfl,
+  positivity,
+end
+
 open_locale ennreal nnrat nnreal
 
 universe u