ink

def Std.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.

Equations

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

ink

def Std.Tactic.seq_focus : 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.