- **The Ln-exact-show tactic is used in LeanNotes snippets in place the of [[exact-tactic|exact]]tactic.** ## Summary The `exact show ... from ...` LeanNotes style tactic 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 instead 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. ### Examples ### proof that implication is transitive: ```lean -- `->` is transitive. example : (P → Q) → (Q → R) → P → R := by intro (hPtoQ : P → Q) (hQtoR : Q -> R) (hP : P) apply hPtoQ at hP; rename' (hP : Q) => hQ -- MP yields hQ : Q apply hQtoR at hQ; rename' (hQ : R) => hR -- MP yields hR : R exact show R from hR -- the LeanNotes-style ``` --- ## References [Bhavik Mehta in Formalizing Mathematics 2025.](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/exact.html#exact)