split … using

split, followed by a per-goal rename_i so the hypotheses it introduces arrive named.

def CustomPrelude.Tactic.«tacticSplit_Using___|» : Lean.ParserDescr

A version of split that also renames the hypotheses introduced.

Equations

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