Additional declarations for Lean.Meta.Tactic.Rewrite

def Lean.Expr.rewrite (e eq : Expr) : MetaM Expr

Rewrites e via some eq, producing a proof e = e' for some e'.

Rewrites with a fresh metavariable as the ambient goal. Fails if the rewrite produces any subgoals.

def Lean.Expr.rewriteType (e eq : Expr) : MetaM Expr

Rewrites the type of e via some eq, then moves e into the new type via Eq.mp.

Rewrites with a fresh metavariable as the ambient goal. Fails if the rewrite produces any subgoals.