injections … with

injections, followed by a rename_i so the equalities it introduces arrive named.

def CustomPrelude.Tactic.tacticInjectionsWith___ : Lean.ParserDescr

injections, naming the hypotheses it introduces.

Equations

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