## exact show P from hP : P Provide explicit `term : type`information to close a proof. ```lean example (hP : P) : P := by exact show P from hP : P -- hP is a term of type: P, `QED` ```