mathlib3 documentation

tactic.wlog

Without loss of generality tactic #

The tactic wlog h : P will add an assumption h : P to the main goal, and add a new goal that requires showing that the case h : ¬ P can be reduced to the case where P holds (typically by symmetry). The new goal will be placed at the top of the goal stack.

A helper function to retrieve the names of the first n arguments to a Pi-expression.

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 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.

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 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.