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 := { transparency := Meta.TransparencyMode.reducible, offsetCnstrs := true, occs := Meta.Occurrences.all, newGoals := Meta.ApplyNewGoals.nonDependentFirst }) : MetaM Meta.RewriteResult

Rewrite goal mvarId

Equations

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