## Summary The [[Ln-exact-show-tactic|exact show ... from ...]] tactic phrase is self-commenting in that it asserts the [[Syntactic, Definitional, and Propositional Equality#Definitional equality|definitional equality]] of the goal and a matching type. For example, if a goal is closed by applying exact hP then it can be closed by providing additional typing information that explicitly documents the match between the goal and a witnessed . exact show P from hP : P The [[Ln-exact-show-tactic|exact show ... from ...]] tactic *syntactically validates* both the goal and the matching context type. This provides more information that the `exact` tactic, which validates only the matching context type. eBook: [exact — Formalising Mathematics 0.1 documentation](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/exact.html) ## Formalizing Math definition [Formalizing Math definition](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/exact.html#summary "Link to this heading") If your goal is `⊢ P` then `exact h` will close the goal if the context contains a type that is [[Syntactic, Definitional, and Propositional Equality#Definitional equality|definitionally equal ]] to the goal. 1. If the local context is h : P ⊢ P then the tactic `exact h` will close the goal. 2. `exact` works up to [definitional equality](https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#defeq). So for example, if the local context is h : ¬ P ⊢ P → False then `exact h` will work, because the type of `h` is definitionally equal to the goal. ### Example ### 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)