- [[assumption-loop-tactic|assumption-loop]] : Loop through subgoals to match types with a hypotheses. For example, the following Lean phrase attempts to match each subgoal that is constructed by the `constructor`tactic with an assumed hypothesis: `constructor <;> assumption` The `<;>` means - evaluate the `constructor` tactic and then - loop through the constructed subgoals and for the current subgoal: - evaluate the `assumption` tactic try to find a hypothesis that matches the current subgoal .