def Lean.Meta.tryURefl (mvarId : MVarId) : MetaM Bool

Try to close goal using rfl with smart unfolding turned off.

def Lean.Meta.getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name)

Returns the "const unfold" theorem (f.eq_unfold) for the given declaration. This is not extensible, and always builds on the unfold theorem (f.eq_def).