- [[assumption-loop-tactic|assumption-loop]] : Loop through subgoals to match with a hypotheses within the subgoal context. 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. **Source** [Formalising Mathematics - Metha](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/assumption.html) <iframe src="https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/assumption.html#:~:text=apply,-%EF%83%81" width="100%" height="700px"></iframe>