structure Lean.Meta.RewriteResult : Type

• eNew : Expr
• eqProof : Expr
• mvarIds : List MVarId

def Lean.MVarId.rewrite (mvarId : MVarId) (e heq : Expr) (symm : Bool := false) (config : Meta.Rewrite.Config := { }) : MetaM Meta.RewriteResult

Rewrite e using heq in the context of mvarId. Returns the result of the rewrite, the metavariable mvarId is not assigned.