The permutation tactics perm, perma, and linperm for the symmetric area and angle relations, along with the helper splitAll and push_contra tactics. These normalize the point arguments of the geometric primitives using the symmetry lemmas from Tactics.

def Lean.Elab.Tactic.getNthArgName (tgt : Expr) (n : ℕ) : MetaM Name

Definitions for perm tactic

Equations

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

def Lean.Elab.Tactic.lte (n1 n2 : Name) : Bool

Definitions for perm tactic

Equations

• Lean.Elab.Tactic.lte n1 n2 = (n1.lt n2 || decide (n1 = n2))

def Lean.Elab.Tactic.convAreaNf : ParserDescr

Conv tactic areaNf

A conv tactic for permuting the variables in an area expression. A building block for the perm tactic.

Equations

• Lean.Elab.Tactic.convAreaNf = Lean.ParserDescr.node `Lean.Elab.Tactic.convAreaNf 1024 (Lean.ParserDescr.nonReservedSymbol "areaNf" false)

def Lean.Elab.Tactic.convColinearNf : ParserDescr

Conv tactic colinearNf

A conv tactic for permuting the variables in an colinear expression. A building block for the perm tactic.

Equations

• Lean.Elab.Tactic.convColinearNf = Lean.ParserDescr.node `Lean.Elab.Tactic.convColinearNf 1024 (Lean.ParserDescr.nonReservedSymbol "colinearNf" false)

def Lean.Elab.Tactic.convTriangleNf : ParserDescr

Conv tactic triangleNf

A conv tactic for permuting the variables in an triangle expression. A building block for the perm tactic.

Equations

• Lean.Elab.Tactic.convTriangleNf = Lean.ParserDescr.node `Lean.Elab.Tactic.convTriangleNf 1024 (Lean.ParserDescr.nonReservedSymbol "triangleNf" false)

def Lean.Elab.Tactic.convLengthNf : ParserDescr

Conv tactic lengthNf

A conv tactic for permuting the variables in an length expression. A building block for the perm tactic.

Equations

• Lean.Elab.Tactic.convLengthNf = Lean.ParserDescr.node `Lean.Elab.Tactic.convLengthNf 1024 (Lean.ParserDescr.nonReservedSymbol "lengthNf" false)

def Lean.Elab.Tactic.convAngleNf : ParserDescr

Conv tactic angleNf

A conv tactic for permuting the variables in an angle expression. A building block for the perm tactic.

Equations

• Lean.Elab.Tactic.convAngleNf = Lean.ParserDescr.node `Lean.Elab.Tactic.convAngleNf 1024 (Lean.ParserDescr.nonReservedSymbol "angleNf" false)

def Lean.Elab.Tactic.convSamesideNf : ParserDescr

Conv tactic samesideNf

A conv tactic for permuting the variables in an sameside expression. A building block for the perm tactic.

Equations

• Lean.Elab.Tactic.convSamesideNf = Lean.ParserDescr.node `Lean.Elab.Tactic.convSamesideNf 1024 (Lean.ParserDescr.nonReservedSymbol "samesideNf" false)

def Lean.Elab.Tactic.convDiffsideNf : ParserDescr

Conv tactic diffsideNf

A conv tactic for permuting the variables in an diffside expression. A building block for the perm tactic.

Equations

• Lean.Elab.Tactic.convDiffsideNf = Lean.ParserDescr.node `Lean.Elab.Tactic.convDiffsideNf 1024 (Lean.ParserDescr.nonReservedSymbol "diffsideNf" false)

def Lean.Elab.Tactic.convParaNf : ParserDescr

Conv tactic paraNf

A conv tactic for permuting the variables in an para expression. A building block for the perm tactic.

Equations

• Lean.Elab.Tactic.convParaNf = Lean.ParserDescr.node `Lean.Elab.Tactic.convParaNf 1024 (Lean.ParserDescr.nonReservedSymbol "paraNf" false)

def Lean.Elab.Tactic.«tacticPerm[_]Only[_]_» : ParserDescr

Tactic perm

A custom experimental tactic for permuting the variables in geometric primitives. The ordering is the one in which the variables are introduced, so it is not necessarily lexigraphic in general. Usage:

• perm permutes the variables in the goal
• perm at h permutes the variables in hypothesis h
• perm at * permutes the variables in the goal and all hypotheses
• perm [t1 t2 ...] adds permuted proof terms t1, t2, ... to the local context, then runs perm In each of these variants but the last, perm can be replaced with perm only [perm_type], where perm_type is one of area, colinear, triangle, length, angle, sameside, diffside.

Equations

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

def Lean.Elab.Tactic.haveExpr (n : Name) (h : Expr) : TacticM Unit

Definitions for perm tactic

Equations

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

def Lean.Elab.Tactic.«tacticHavePerms[_]» : ParserDescr

Definitions for perm tactic

Equations

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

def Lean.Elab.Tactic.tacticAssumptionSymm : ParserDescr

Definitions for perm tactic

Equations

• Lean.Elab.Tactic.tacticAssumptionSymm = Lean.ParserDescr.node `Lean.Elab.Tactic.tacticAssumptionSymm 1024 (Lean.ParserDescr.nonReservedSymbol "assumptionSymm" false)

def Lean.Elab.Tactic.«tacticPerma[_]Only[_]_» : ParserDescr

Tactic perma

Like perm, but also tries to exact assumptions and their symmetrized versions.

Equations

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

def Lean.Elab.Tactic.«tacticLinperm[_]» : ParserDescr

Tactic linperm

A combination of linarith and perm. Usage:

• linperm runs perm at * followed by linarith
• linperm [t1 t2 ...] runs perm at *, adds permuted proof terms t1, t2, ... to the local context, and finishes with linarith

Equations

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

def Lean.Elab.Tactic.tacticSplitAll : ParserDescr

Tactic for breaking ands up

Equations

• Lean.Elab.Tactic.tacticSplitAll = Lean.ParserDescr.node `Lean.Elab.Tactic.tacticSplitAll 1024 (Lean.ParserDescr.nonReservedSymbol "splitAll" false)

def Lean.Elab.Tactic.tacticPush_contra__ : ParserDescr

by_contra followed by push Not

Equations

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