- [[apply-tactic|apply <Conditional>]] : If - a conditional term is assumed, and - the goal is its conclusion type, - then change the goal to its premise type, so that it suffices to prove the premise. **NOTE:** The article below also includes a description of the tactic: - [[apply-at-tactic|apply <Conditional> at <Premise>]] : Apply modus ponens. **Source:** [Formalizing Mathematics - Metha](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html) <iframe src="https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html#:~:text=apply,-%EF%83%81" width="100%" height="700px"></iframe> --- Author: [[dducoff]] Posted Date: 2026-06-25