Lean4
/-- `wlog h : P` will add an assumption `h : P` to the main goal, and add a side goal that requires
showing that the case `h : ¬ P` can be reduced to the case where `P` holds (typically by symmetry).
The side goal will be at the top of the stack. In this side goal, there will be two additional
assumptions:
- `h : ¬ P`: the assumption that `P` does not hold
- `this`: which is the statement that in the old context `P` suffices to prove the goal.
By default, the name `this` is used, but the idiom `with H` can be added to specify the name:
`wlog h : P with H`.
Typically, it is useful to use the variant `wlog h : P generalizing x y`,
to revert certain parts of the context before creating the new goal.
In this way, the wlog-claim `this` can be applied to `x` and `y` in different orders
(exploiting symmetry, which is the typical use case).
By default, the entire context is reverted. -/
@[tactic_parser 1000]
public meta def wlog : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.wlog 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "wlog " false✝) Lean.binderIdent)
(ParserDescr.symbol✝ " : "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " generalizing")
(ParserDescr.unary✝ `many
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.const✝ `ident))))))
(ParserDescr.unary✝ `optional (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with ") Lean.binderIdent)))
