t <;> [t₁ | t₂ | …]

seq_focus's own notation, respelled with | separators to pair with the project's other bracketed tactic lists.

def CustomPrelude.Tactic.«tactic_<;>[_|]» : Lean.TrailingParserDescr

t <;> [t1; t2; ...; tn] focuses on the first goal and applies t, which should result in n subgoals. It then applies each ti to the corresponding goal and collects the resulting subgoals.

Equations

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