[[intro-tactic|intro]] : Reduce a conditional goal to its conclusion by assuming its premises. **IDIOM:** refer to the LeanNotes idiom, [[intro-format]], which provides a description for each hypotheses. [intro tactic - Formalizing Mathematics - Metha](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/intro.html) <iframe src="https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/intro.html#:~:text=apply,-%EF%83%81" width="100%" height="700px"></iframe> --- Author: [[dducoff]] Posted Date: 2026-06-25