## exact-show - [[exact-show]]` : Include the `term : type` information when closing a goal. ```lean example (hP : P) : P := by exact show P from hP -- hP is a term of type: P, `QED` ``` ## Syntax exact `<Goal Type>` show from `<Hypotheses>`, where the `Hypotheses` term is a witness of the `Goal type`. ## Description The [[Tactics/exact-tactic|exact]] tactic specifies the `hypotheses`term that is witness of the `goal`type. This LeanNotes idiom conforms to the [[type-binding rule]] that binds a term to its type explicitly.