# Documentation

Mathlib.Tactic.Relation.Symm

# symm tactic #

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

Environment extensions for symm lemmas

def Lean.Expr.symmAux {α : Type} (tgt : Lean.Expr) (k : ) :

Internal implementation of Lean.Expr.symm, Lean.MVarId.symm, and the user-facing tactic.

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

k lem args body should calculate a result, given a candidate symm lemma lem, which will have type ∀ args, body∀ args, body.

In Lean.Expr.symm this result will be a new Expr, and in Lean.MVarId.symm and Lean.MVarId.symmAt this result will be a new goal.

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

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

Equations
• One or more equations did not get rendered due to their size.
def Lean.MVarId.symmAux (tgt : Lean.Expr) (k : ) (g : Lean.MVarId) :

Internal implementation of Lean.MVarId.symm and the user-facing tactic.

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

k lem args body goal should transform goal into a new goal, given a candidate symm lemma lem, which will have type ∀ args, body∀ args, body. Depending on whether we are working on a hypothesis or a goal, k will internally use either replace or assign.

Equations

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

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

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

Equations

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

Equations
• One or more equations did not get rendered due to their size.
• symm applies to a goal whose target has the form t ~ u where ~ is a symmetric relation, that is, a relation which has a symmetry lemma tagged with the attribute [symm]. It replaces the target with u ~ t.
• symm at h will rewrite a hypothesis h : t ~ u to h : u ~ t.
Equations
• One or more equations did not get rendered due to their size.

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

Equations