Documentation

Mathlib.Tactic.Substs

The substs macro #

The substs macro applies the subst tactic to a list of hypothesis, in left to right order.

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

Applies the subst tactic to all given hypotheses from left to right.

Equations
    Instances For