structure Lean.Meta.RewriteResult : Type

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

def Lean.MVarId.rewrite (mvarId : Lean.MVarId) (e : Lean.Expr) (heq : Lean.Expr) (symm : optParam Bool false) (config : optParam Lean.Meta.Rewrite.Config { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true, occs := Lean.Meta.Occurrences.all, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst }) : Lean.MetaM Lean.Meta.RewriteResult

Rewrite goal mvarId

Equations

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