Tactic cheatsheet

If you think you know which part of the tactic state your “next move” should relate to (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 (if goal is Q) or apply h at...
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	constructor	cases' h with hP hQ
P ↔ Q	constructor	rw h (or cases' h with h1 h2)
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