def Aesop.replaceFVar (goal : Lean.MVarId) (fvarId : Lean.FVarId) (type proof : Lean.Expr) : Lean.MetaM (Lean.MVarId × Lean.FVarId × Bool)

A MetaM version of the replace tactic. If fvarId refers to the hypothesis h, this tactic asserts a new hypothesis h : type with proof proof : type and then tries to clear fvarId. Unlike replaceLocalDecl, replaceFVar always adds the new hypothesis at the end of the local context.

replaceFVar returns the new goal, the FVarId of the newly asserted hypothesis and whether the old hypothesis was cleared.

def Aesop.introsUnfolding (mvarId : Lean.MVarId) : Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Introduce as many binders as possible while unfolding definitions with the ambient transparency.

partial def Aesop.introsUnfolding.run (mvarId : Lean.MVarId) (fvars : Array Lean.FVarId) : Lean.MetaM (Array Lean.FVarId × Lean.MVarId)