Wlog in the usual sense

Stream: Is there code for X?

[Vincent Beffara]

Is there a tactic that does what is usually meant by wlog in math papers? More precisely, assuming the goal is to show some property of a function f, saying suffices (f 0 = 0) generalizing f would split the situation into

• the current one with the additional assumption f 0 = 0
• a new situation with an additional assumption saying "for every function with g 0 = 0 plus all the other assumptions on f transported into assumptions on g, the corresponding goal holds" (and then your job is to massage f into g satisfying the assumption and use the lemma).

So, something a little bit similar to suffices but that would generate an intermediate lemma. I'm guessing that this can be done using a mixture of suffices and revert, and of course when the separate lemma is of more general use it is always possible to state it explicitly, but it would be useful as a standalone tactic.

[Johan Commelin]

See this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/wlog.20tactic.20.3A.20documentation.2Fhowto.3F

[Alex J. Best]

I'd like to get one version or the other into mathlib for sure!

[Vincent Beffara]

Ah, thanks, I had missed that thread and indeed wlog' described there does what I am asking for, it I understand it right. I will try to give it a try...

[Vincent Beffara]

... yep, that's exactly what I had in mind. It would certainly be useful to have it in mathlib!