- [[assumption-tactic|assumption]] : Search the hypotheses for a match with the goal. NOTE: For closing one goal, use the [[exact-show]] idiom. For closing multiple goals implicitly, use this tactic together with the `<;>` do operator. The article below mentions this near the end article: - You can do `constructor <;> assumption`. The `<;>` means “do `constructor` and then do `assumption` on all goals produced by `constructor` tactic. **Source:** [Formalizing 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> - Suggested comment style: ```lean assumption -- The goal is witnessed by `hP`. ``` --- **`LeanNotes curator:`** [[dducoff]] **`Posted Date:`** 2026-08-11