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.

Equations

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

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.

Equations

• Aesop.introsUnfolding mvarId = Aesop.introsUnfolding.run mvarId #[]

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