def Lean.Meta.substCore (mvarId : MVarId) (hFVarId : FVarId) (symm : Bool := false) (fvarSubst : FVarSubst := { }) (clearH : Bool := true) (tryToSkip : Bool := false) : MetaM (FVarSubst × MVarId)

def Lean.Meta.heqToEq (mvarId : MVarId) (fvarId : FVarId) (tryToClear : Bool := true) : MetaM (FVarId × MVarId)

Given h : HEq α a α b in the given goal, produce a new goal where h : Eq α a b. If h is not of the give form, then just return (h, mvarId)

def Lean.Meta.substVar (mvarId : MVarId) (x : FVarId) : MetaM MVarId

Given x, try to find an equation of the form heq : x = rhs or heq : lhs = x, and runs substCore on it. Throws an exception if no such equation is found.

partial def Lean.Meta.subst (mvarId : MVarId) (h : FVarId) : MetaM MVarId

def Lean.Meta.subst.substEq (mvarId : MVarId) (h : FVarId) : MetaM MVarId

Give h : Eq α a b, try to apply substCore

def Lean.Meta.substVar? (mvarId : MVarId) (hFVarId : FVarId) : MetaM (Option MVarId)

Given x, try to find an equation of the form heq : x = rhs or heq : lhs = x, and runs substCore on it. Returns none if no such equation is found, or if substCore fails.

def Lean.Meta.subst? (mvarId : MVarId) (hFVarId : FVarId) : MetaM (Option MVarId)

def Lean.Meta.substCore? (mvarId : MVarId) (hFVarId : FVarId) (symm : Bool := false) (fvarSubst : FVarSubst := { }) (clearH : Bool := true) (tryToSkip : Bool := false) : MetaM (Option (FVarSubst × MVarId))

def Lean.Meta.trySubstVar (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId

def Lean.Meta.trySubst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId

def Lean.Meta.substSomeVar? (mvarId : MVarId) : MetaM (Option MVarId)

partial def Lean.Meta.substVars (mvarId : MVarId) : MetaM MVarId