[Merged by Bors] - feat(tactic/monotonicity): Allow @[mono] on strict_mono lemmas

[eric-wieser]

A follow-up to #3310

---

[fpvandoorn]

Can you add a test to the test folder to show that this works as expected?

[eric-wieser]

I added a test, but all it checks is that @[mono] no longer rejects strict_mono. I can't work out how the mono tactic is supposed to be used with monotone and nor is that tested, so I can't add a test that actually exercises strict_mono.

edit: oh, we have monotonicity.lean and monotonicity/test_cases.lean which both test this tactic.

[fpvandoorn]

I can't work out how the mono tactic is supposed to be used with monotone and nor is that tested, so I can't add a test that actually exercises strict_mono.

I think that is tested here: https://github.com/leanprover-community/mathlib/blob/coe_minmax/test/monotonicity.lean#L114-L152
The mono tactic should at least work with strict_mono lemmas for this PR to be merged, otherwise this PR is useless. I don't know how hard-coded monotone is in the mono tactic, but maybe the tactic needs to change to accept strict_mono assumptions.

[eric-wieser]

Resolved - there were two different test files that seem not to be aware of each other, and I found the one that didn't have any hints of how to write the tests.

[semorrison]

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests