Tactic cheatsheet

If you think you know which part of the tactic state your “next move” should be (i.e. you know whether you should be manipulating the goal or using a hypothesis) then the below table might give you a hint as to which tactic to use.

Cheat sheet

Form of proposition	In the goal?	Hypothesis named h?
P → Q	intro hP	apply h
true	trivial	(can’t be used)
false	(can’t be used)	exfalso, exact h or cases h
¬P	intro hP	apply h (if goal is false)
P ∧ Q	split	cases h with hP hQ
P ↔ Q	split	cases h or rw h
P ∨ Q	left or right	cases h with hP hQ
∀ (a : X), ...	intro x	specialize h x
∃ (a : X), ...	use x	cases h with x hx