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

The result of running `wlog`

on a goal.

- reductionGoal : Lean.MVarId
The

`reductionGoal`

requires showing that the case`h : ¬ P`

can be reduced to the case where`P`

holds. It has two additional assumptions in its context:`h : ¬ P`

: the assumption that`P`

does not hold`H`

: the statement that in the original context`P`

suffices to prove the goal.

- reductionFVarIds : Lean.FVarId × Lean.FVarId
The pair

`(HFVarId, negHypFVarId)`

of`FVarIds`

for`reductionGoal`

:`HFVarId`

:`H`

, the statement that in the original context`P`

suffices to prove the goal.`negHypFVarId`

:`h : ¬ P`

, the assumption that`P`

does not hold

- hypothesisGoal : Lean.MVarId
The original goal with the additional assumption

`h : P`

. - hypothesisFVarId : Lean.FVarId
The

`FVarId`

of the hypothesis`h`

in`hypothesisGoal`

- revertedFVarIds : Array Lean.FVarId
The array of

`FVarId`

s that was reverted to produce the reduction hypothesis`H`

in`reductionGoal`

, which are still present in the context of`reductionGoal`

(but not necessarily`hypothesisGoal`

).

## Instances For

`wlog goal h P xs H`

will return two goals: the `hypothesisGoal`

, which adds an assumption
`h : P`

to the context of `goal`

, and the `reductionGoal`

, which requires showing that the case
`h : ¬ P`

can be reduced to the case where `P`

holds (typically by symmetry).

In `reductionGoal`

, there will be two additional assumptions:

`h : ¬ P`

: the assumption that`P`

does not hold`H`

: which is the statement that in the old context`P`

suffices to prove the goal. If`H`

is`none`

, the name`this`

is used.

If `xs`

is `none`

, all hypotheses are reverted to produce the reduction goal's hypothesis `H`

.
Otherwise, the `xs`

are elaborated to hypotheses in the context of `goal`

, and only those
hypotheses are reverted (and any that depend on them).

If `h`

is `none`

, the hypotheses of types `P`

and `¬ P`

in both branches will be inaccessible.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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

## Equations

- One or more equations did not get rendered due to their size.