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). wlog! h : P is a variant that will also call push_neg at h : ¬ P.

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.

def Mathlib.Tactic.wlogCore (h : Lean.TSyntax `Lean.binderIdent) (P : Lean.Term) (xs : Option (Lean.TSyntaxArray `ident)) (H : Option (Lean.TSyntax `ident)) (pushConfig : Option (Lean.TSyntax `Lean.Parser.Tactic.optConfig) := none) : Lean.Elab.Tactic.TacticM Unit

The implementation of wlog and wlog!

def Mathlib.Tactic.wlog : Lean.ParserDescr

wlog h : P adds an assumption h : P to the main goal, and adds 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 entire context is reverted to produce this.

• wlog h : P with H gives the name H to the statement that P proves the goal.
• wlog h : P generalizing x y ... reverts 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).
• wlog! h : P also calls push_neg at the generated hypothesis h. wlog! h : P ∧ Q will transform ¬ (P ∧ Q) to P → ¬ Q
• wlog! +distrib h : P also calls push_neg +distrib at the generated hypothesis h. wlog! +distrib h : P ∧ Q will transform ¬ (P ∧ Q) to ¬P ∨ ¬Q.

def Mathlib.Tactic.wlog! : Lean.ParserDescr

wlog h : P adds an assumption h : P to the main goal, and adds 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 entire context is reverted to produce this.

• wlog h : P with H gives the name H to the statement that P proves the goal.
• wlog h : P generalizing x y ... reverts 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).
• wlog! h : P also calls push_neg at the generated hypothesis h. wlog! h : P ∧ Q will transform ¬ (P ∧ Q) to P → ¬ Q
• wlog! +distrib h : P also calls push_neg +distrib at the generated hypothesis h. wlog! +distrib h : P ∧ Q will transform ¬ (P ∧ Q) to ¬P ∨ ¬Q.