symm tactic

This implements the symm tactic, which can apply symmetry theorems to either the goal or a hypothesis.

opaque Lean.Meta.Symm.symmExt : SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name)

Environment extensions for symm lemmas

def Lean.Expr.getSymmLems (tgt : Expr) : MetaM (Array Name)

Return the symmetry lemmas that match the target type.

def Lean.Expr.applySymm (e : Expr) : MetaM Expr

Given a term e : a ~ b, construct a term in b ~ a using @[symm] lemmas.

def Lean.MVarId.applySymm (g : MVarId) : MetaM MVarId

Apply a symmetry lemma (i.e. marked with @[symm]) to a metavariable.

The type of g should be of the form a ~ b, and is used to index the symm lemmas.

def Lean.MVarId.applySymmAt (h : FVarId) (g : MVarId) : MetaM MVarId

Use a symmetry lemma (i.e. marked with @[symm]) to replace a hypothesis in a goal.

def Lean.MVarId.symmSaturate (g : MVarId) : MetaM MVarId

For every hypothesis h : a ~ b where a @[symm] lemma is available, add a hypothesis h_symm : b ~ a.