`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

- Mathlib.Tactic.rflTac = Lean.Elab.Tactic.withMainContext (Lean.Elab.Tactic.liftMetaFinishingTactic fun (x : Lean.MVarId) => x.applyRfl)

## 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.