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.

def Lean.Meta.substEq (mvarId : MVarId) (hFVarId : FVarId) (fvarSubst : FVarSubst := { }) : MetaM (FVarSubst × MVarId)

If hFVarId is an Eq (or a HEq that can be turned into an Eq) with a free variable on the LHS or RHS, eliminates the variable by substitution.

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

def Lean.Meta.introSubstEq (mvarId : MVarId) (substLHS : Bool := false) : MetaM (FVarSubst × MVarId)

Given a goal (a = b) → goal[b], creates a new goal goal[a], clearing b.

This is essentially intro h; subst h, but in the case that b is a free variable and has no forward dependencies implements this without introducing the equality, which can make a difference in terms of performance.

If substLHS = true, assume (a = b) → goal[a] and create goal goal[b], clearing a.

Also handles heterogeneous equalities in cases where eq_of_heq would apply.

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