assumption

assumption solves goals in which there exists an assumption that directly proves the goal (no simplification). This tactic will fail if there does not exist such an assumption.

Syntax

(* Simple usage *)
assumption.

Examples

Before

P: Prop
H: P
=========================
1/1
P

assumption.

After

No more goals.

Resources

Reference Documentation

---