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 goal mvarId

Equations

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