symm
tactic #
This implements the symm
tactic, which can apply symmetry theorems to either the goal or a
hypothesis.
Environment extensions for symm lemmas
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
.
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.
Instances For
Given a term e : a ~ b
, construct a term in b ~ a
using @[symm]
lemmas.
Instances For
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
.
Depending on whether we are working on a hypothesis or a goal,
k
will internally use either replace
or assign
.
Instances For
Apply a symmetry lemma (i.e. marked with @[symm]
) to a metavariable.
Instances For
Use a symmetry lemma (i.e. marked with @[symm]
) to replace a hypothesis in a goal.
Instances For
For every hypothesis h : a ~ b
where a @[symm]
lemma is available,
add a hypothesis h_symm : b ~ a
.
Instances For
For every hypothesis h : a ~ b
where a @[symm]
lemma is available,
add a hypothesis h_symm : b ~ a
.