exact

exact allows users to solve goals by providing a proof object directly. This tactic will fail if the provided proof object does not prove the goal.

Syntax

(* Simple usage *)
exact I.

Examples

Before

-------------------------
1/1
True

exact I.

After

Proof finished

Before

n: nat
-------------------------
1/1
n + 5 = n + 5

exact (eq_refl (n + 5)).

After

Proof finished

Resources

Reference Documentation

---