def Lean.Elab.Tactic.elabRewrite (mvarId : MVarId) (e : Expr) (stx : Syntax) (symm : Bool := false) (config : Meta.Rewrite.Config := { }) : TacticM Meta.RewriteResult

Runs Lean.MVarId.rewrite, and also handles filtering out the old metavariables in the rewrite result. This should be used from within withSynthesize. Use finishElabRewrite once elaboration is complete to make final updates to RewriteResult.

def Lean.Elab.Tactic.finishElabRewrite (r : Meta.RewriteResult) : MetaM Meta.RewriteResult

Makes new goals be synthetic opaque, to be done once elaboration of the rewrite theorem is complete.

Workaround note: we are only doing this for proof goals, not data goals, since there are many downstream cases of tactic proofs that later assign data goals by unification.

def Lean.Elab.Tactic.rewriteTarget (stx : Syntax) (symm : Bool) (config : Meta.Rewrite.Config := { }) : TacticM Unit

def Lean.Elab.Tactic.rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Meta.Rewrite.Config := { }) : TacticM Unit

def Lean.Elab.Tactic.withRWRulesSeq (token rwRulesSeqStx : Syntax) (x : Bool → Syntax → TacticM Unit) : TacticM Unit

def Lean.Elab.Tactic.elabRewriteConfig : Syntax → TacticM Meta.Rewrite.Config

def Lean.Elab.Tactic.evalRewriteSeq : Tactic