||

The infix || tactical tries the first tactic and only tries the second if the first failed. In other words, || executes the first tactic that makes progress on the goal.

Syntax

(* Simple usage *)
reflexivity || assumption.

Examples

Before

P: Prop
H: P
-------------------------
1/1
P

reflexivity || assumption.

After

Proof finished

Resources

Reference Documentation

---