rfl tactic extension for reflexive relations

This extends the rfl tactic so that it works on any reflexive relation, provided the reflexivity lemma has been marked as @[refl].

opaque Lean.Meta.Rfl.reflExt : SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name)

Environment extensions for refl lemmas

def Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit

MetaM version of the rfl tactic.

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

Equations

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

@[deprecated "`rel_of_eq_and_refl` is unused in core; copy it downstream if you need it." (since := "2026-09-09")]

theorem Lean.Meta.Rfl.rel_of_eq_and_refl {α : Sort u_1} {R : α → α → Prop} {x y : α} (hxy : x = y) (h : R x x) : R x y

Helper theorem for Lean.MVarId.liftReflToEq.

@[deprecated "`Lean.MVarId.liftReflToEq` is unused in core; copy it downstream if you need it." (since := "2026-09-09")]

def Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM 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.