Function any_goals 

pub fn any_goals(t: Tactic) -> Tactic

t1 <;> t2-style: apply t to EVERY goal currently open (not just the focused one). Each goal is focused in turn; the subgoals t produces for it become the new open set, in original goal order. any_goals t: run t on every open goal, keeping the goals it left and the goals it declined alike, and succeed iff it succeeded on AT LEAST ONE.

The permissive sibling of all_goals, and the one Lean scripts actually reach for after a constructor splits a goal into branches only some of which t can discharge. Unlike all_goals it does not abort the whole combinator when t fails on one branch — that branch is simply carried forward unchanged.