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.

structure Mathlib.Tactic.WLOGResult : Type

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 FVarIds that was reverted to produce the reduction hypothesis H in reductionGoal, which are still present in the context of reductionGoal (but not necessarily hypothesisGoal).

def Lean.MVarId.wlog (goal : MVarId) (h : Option Name) (P : Expr) (xs : Option (TSyntaxArray `ident) := none) (H : Option Name := none) : Elab.Tactic.TacticM Mathlib.Tactic.WLOGResult

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.

def Mathlib.Tactic.wlog : Lean.ParserDescr

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.