Documentation

Mathlib.Tactic.Relation.Rfl

Lean.MVarId.liftReflToEq #

Convert a goal of the form x ~ y into the form x = y, where ~ is a reflexive relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl]. If this can't be done, returns the original MVarId.

This tactic applies to a goal whose target has the form x ~ x, where ~ is a reflexive relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].

Equations
Instances For

    If e is the form @R .. x y, where R is a reflexive relation, return some (R, x, y). As a special case, if e is @HEq α a β b, return some (`HEq, a, b).

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

      Convert a goal of the form x ~ y into the form x = y, where ~ is a reflexive relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl]. If this can't be done, returns the original MVarId.

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