assumption

Summary

The assumption tactic closes a goal ⊢ P when there is a hypothesis h : P. Note that exact h also closes this goal, and is shorter too, so only use this when the name of the hypothesis is five or more letters long ;-) Other uses include when one is trying to be clever and using ; instead of , at the end of a tactic, to try and prove more than one goal at once.

Examples

Faced with the goal

reallylonghypothesisname : P
h1 : Q
h2 : 2 + 2 = 5
...
h100 : x = x
⊢ P

you could do exact reallylonghypothesisname but assumption works as well. Although what are you doing with a really long hypothesis name?

If your tactic state is

hP : P
hQ : Q
⊢ P ∧ Q

you can do split; assumption. The semicolon, used instead of a comma, means “do split and then do assumption on all goals produced by split”.

Further notes

If you decide that you are interested in learning how to write tactics then assumption is usually a good one to try and write. Rob Lewis has made some excellent videos on tactic writing at insert link here. Note that there will be nothing about tactic writing in this course because the author doesn’t have the first clue about it.