positivity

Stream: mathlib4

[Heather Macbeth]

@David Renshaw Thank you for the positivity extensions you are churning out!!

If you would like a suggestion for one to do next: there is a broken positivity call in #1304 (worked around for now)
https://github.com/leanprover-community/mathlib4/blob/1bf3ce67445f01212cf926aa4cca7b1a6e8166fd/Mathlib/Algebra/Order/Floor.lean#L1045
where apparently the problem is the lack of the docs#positivity_coe extension.

[Yury G. Kudryashov]

Is there any documentation about writing positivity extensions in mathlib4?

[Jeremy Tan]

Yes. How can I get the first positivity extension in !4#4409 to work?

[Jeremy Tan]

The second one has been made to work, but the first requires extracting a hypothesis of the right type from context for which there is absolutely no documentation or precedent to work from

[Jeremy Tan]

I've included the original mathlib3 code there. Anyone?

[Kyle Miller]

@Jeremy Tan I wrote a new little tactic macro to drive positivity for this file. It seems like having it be a positivity extension isn't a good match for mathlib4's positivity anymore.