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.

def Mathlib.Tactic.rflTac : Lean.Elab.Tactic.TacticM Unit

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.applyRfl x)

def Lean.MVarId.liftReflToEq (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

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.