| [[Tactics/intro-tactic\|intro]] *premise hypotheses* | if the goal is a `conditional`, `⊢ P → Q` <br>then the `premise` can be assumed as a hypotheses, `hP : P`<br>and the goal can be reduced to its `conclusion`, `⊢ Q`,<br>by applying **intro*** `(hP : P)`. | | | -------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | --- | | | | | ## Preferred idiom The preferred LeanNotes idiom, [[intro-typing]], 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-typing]], 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) --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date:`** 2026-08-11