Quick Reference

What tactic do I need? Find the connective in your goal or hypothesis and read across.

---

Logical connectives

	⊢ Goal	Hypothesis h
And P ∧ Q	constructor / exact ⟨p, q⟩	obtain ⟨p, q⟩ := h / h.1, h.2
Or P ∨ Q	left / right	rcases h with p \| q
Implication P → Q	intro p	apply h / exact h p
Negation ¬P	intro p (it is P → False)	exact h p / contradiction
Equivalence P ↔ Q	constructor	rw [h] / h.mp, h.mpr
Inequality a ≠ b	intro h (it is a = b → False)	exact h rfl / contradiction

push_neg simplifies negated compound statements by pushing ¬ inward: ¬∀ becomes ∃ ¬, ¬(P ∧ Q) becomes P → ¬Q, and so on. Works on both goals (push_neg) and hypotheses (push_neg at h).

Equality and arithmetic

	⊢ Goal	Hypothesis h
Equality a = b	rfl	rw [h] / rw [← h]

Use rw [h] at h' to rewrite in a specific hypothesis. Use nth_rw n [h] to rewrite only the n-th occurrence.

Quantifiers

	⊢ Goal	Hypothesis h
Universal ∀ x, P x	intro x	apply h / exact h a
Existential ∃ x, P x	use a	obtain ⟨x, hx⟩ := h

True, False, and closing tactics

	⊢ Goal	Hypothesis h
True	trivial	—
False	exfalso	contradiction

When the goal matches a hypothesis exactly, exact h or assumption closes it.

Tactic mode and term mode

Tactic mode (after by) builds proofs step by step. Term mode constructs proofs directly as expressions. You can mix both freely.

Direction	Syntax	Example
Enter tactic mode	by	theorem ... := by intro p; exact p
Use a term in tactic mode	exact	exact ⟨p, q⟩
Use tactics inside a term	by in subexpression	⟨p, by assumption⟩
Term mode function	fun x => ...	fun p => ⟨p, p⟩
Anonymous constructor	⟨...⟩	⟨h.2, h.1⟩ for Q ∧ P
Field access	.1, .2, .mp, .mpr	h.2 for second component
Function application	f x or f <| x	h₂ (h₁ p) or h₂ <| h₁ p
Composition	g ∘ f	h₃ ∘ h₂ ∘ h₁

Proof structure

Tactic	Effect
have q := h p	Forward step: derive a new fact from existing ones
suffices p : P by ...	Backward step: state what would be enough, then prove it
rintro ⟨p, q⟩ / rintro (p \| q)	Combine intro with pattern matching