# Documentation

## Lean.Meta.Tactic.Subst

def Lean.Meta.substCore (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) (symm : ) (fvarSubst : optParam Lean.Meta.FVarSubst { map := }) (clearH : ) (tryToSkip : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Meta.heqToEq (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (tryToClear : ) :

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)

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
partial def Lean.Meta.subst (mvarId : Lean.MVarId) (h : Lean.FVarId) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Meta.substVar? (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) :

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.

Equations
Instances For
def Lean.Meta.subst? (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) :
Equations
Instances For
def Lean.Meta.substCore? (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) (symm : ) (fvarSubst : optParam Lean.Meta.FVarSubst { map := }) (clearH : ) (tryToSkip : ) :
Equations
Instances For
def Lean.Meta.trySubstVar (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) :
Equations
Instances For
def Lean.Meta.trySubst (mvarId : Lean.MVarId) (hFVarId : Lean.FVarId) :
Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
partial def Lean.Meta.substVars (mvarId : Lean.MVarId) :