Documentation

Lean.Meta.Tactic.Symm

symm tactic #

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

Return the symmetry lemmas that match the target type.

Equations
    Instances For

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

      Equations
        Instances For

          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.

          Equations
            Instances For

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

              Equations
                Instances For

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

                  Equations
                    Instances For