- [[exact-tactic|exact]] : If a hypotheses has the type defined in the goal, then close the goal. **IDIOM:** refer to the LeanNotes idiom, [[exact-show]], which provides `term : type` definition when closing a goal. [exact tactic - Formalizing Mathematics - Metha](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/exact.html) <iframe src="https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/exact.html#:~:text=apply,-%EF%83%81" width="100%" height="700px"></iframe> --- Author: [[dducoff]] Posted Date: 2026-06-25