## intro *conditional-premise* if the goal is a conditional type, `⊢ P → Q` then the goal can be reduced to its conclusion type, `⊢ Q`, by applying **intro*** `hP`, which constructs a new hypotheses, `(hP : P)` ## Preferred idiom The preferred LeanNotes idiom, [[intro-format]], provides the explicit `term : type` definition when closing a goal. For example, if a goal is closed by applying **exact show** `hP`, it can be closed by providing additional explicit type information using the idiom: **exact show** `P` from `hP : P` The point here is to provide *syntactically validated comments* whenever possible. The preferred LeanNotes idiom, [[intro-format]], explicitly types the newly constructed premise hypothesis. - Suggested format: ```lean example : (P → Q) → (Q → R) → P → R := by intro (hPtoQ : P → Q) (hQtoR : Q -> R) (hP : P) ``` ## See also **Source:** [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> --- **`LeanNotes curator:`** [[dducoff]] **`Posted Date:`** 2026-08-11