Mathlib.Tactic.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.

theorem Mathlib.Tactic.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 Mathlib.Tactic.liftReflToEq.

def Mathlib.Tactic.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.

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

def Lean.Expr.relSidesIfRefl? (e : Expr) : MetaM (Option (Name × Expr × Expr))

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.