Documentation

Lean.Meta.Tactic.Symm

symm tactic #

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

Discrimation tree settings for the symm extension.

Equations
Instances For

    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
      • One or more equations did not get rendered due to their size.
      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
        • One or more equations did not get rendered due to their size.
        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
            • One or more equations did not get rendered due to their size.
            Instances For