The substs macro

The substs macro is a deprecated version of the subst tactic that allowed for more than one hypothesis. Since subst now also supports multiple hypotheses, substs is deprecated.

def Mathlib.Tactic.Substs.substs : Lean.ParserDescr

Deprecated: this functionality exists in subst now.

Equations

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