This PR, specifically support for mono with with, is apparently needed to finish #3419. Please finalise the port in due course.

This PR, specifically support for mono with with, is apparently needed to finish #3419. Please finalise the port in due course.

Heard, will do! :) Note: this will pass CI before it's ready for review. I will mark it ready for review when it's ready for review.

@thorimur is this ready for review?

@thorimur is this ready for review?

Nope, as stated above, I'll put it out for review when it's ready for review. :) (Note the pervasive lack of docstrings!) I'm trying to finish it off today; I also revamped the workings of mono*, and I'm currently refactoring that so that it's not so terrible to review. (Sorry, I might wind up force-pushing your commit away so that I can do some git surgery; I'm working locally as I figure it out.)

Is this PR still relevant? It seems mono made it well and good to Lean 4 already.

@YaelDillies I don't think this PR should go ahead as-is: I feel like the consensus (from a porting meeting a long time ago) was that this PR simply demanded too much review/introduced too much unneeded infrastructure, the current behavior was ok, and that we had another more opinionated tactic (something involving congr?) to help with some specific monotonicity cases anyway.

However, note that lean 3 mono did not make it into mathlib4 as advertised! Currently it still just uses solve_by_elim under the hood (thus it's really closer to mono*), and actually throws errors upon seeing left/right, with, and using syntax.

I feel like there's an argument to be made for intentionally abandoning some of the syntax: mono ... with was essentially an artifact of mono's bespoke backtracking procedure. using could perhaps be incorporated into a solve_by_elim or aesop call. left and right could be useful to someone, and it makes sense to have some way to distinguish between these different sorts of lemmas based on strictness, but I'm not sure calling them "left" and "right" is really a clear, understandable abstraction. Also, @[mono left] and @[mono right] are pretty infrequent. But we should probably discuss this on Zulip (EDIT: now here)

Either way, mono currently does need fixing up, but I'm pretty sure this PR is not the way to do it. There's a chance it might be useful for reference when doing that fixup, but I'd rather reference it as a closed PR instead of an open one. :)