Variants on `mono`

Stream: metaprogramming / tactics

[Heather Macbeth]

I see. I would imagine this to be a non-"fancy" tactic, safe to use at any stage of a proof. (As congr is.). But this question seems implementation-dependent to me so I think it's too early to say for sure. This is just a few lines of prototype code, the point is just to confirm or refute the idea that it's a tactic we'd use -- it would get completely rewritten before joining mathlib.

[Yaël Dillies]

I just encountered a really weird apply/positivity bug: In a very specific case, if the goal I call it on was generated by apply, positivity fails; but if it was generated by refine, positivity succeeds.

[Yaël Dillies]

Here it is.

[Damiano Testa]

I encountered something similar: does instantiating some mvars help?

[Damiano Testa]

I'm on mobile, but there is more context in a PR of mine that was merged earlier today, fixing what I think is a similar big for compute_degree_le