def Batteries.Tactic.«tacticMap_tacs[_;]» : Lean.ParserDescr

Assuming there are n goals, map_tacs [t1; t2; ...; tn] applies each ti to the respective goal and leaves the resulting subgoals. It raises an error if the number of subgoals does not match.

Equations

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

def Batteries.Tactic.seq_focus : Lean.TrailingParserDescr

tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'.

Extensions:

• 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. It raises an error if the number of subgoals does not match.

Equations

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