- [[assumption-tactic|assumption]] : Search the assumed hypotheses to match with the goal. [assumption tactic - Formalizing Mathematics - Metha](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/XXX.html) 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. <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> --- Author: [[dducoff]] Posted Date: 2026