exact

The exact tactic can be used to close a goal.

Example

If the local context is

P : Prop,
HP : P
⊢ P

then the tactic exact HP (note: not exact P) will close the goal.

In this case, because the goal is one of the hypotheses, the assumption tactic would also work fine. However exact is more general, because it takes an arbitrary term. For example, the goal here is not precisely one of the assumptions, it is built from two of them.

try it!

example (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
begin
  /-
  P Q : Prop,
  HP : P,
  HPQ : P → Q
  ⊢ Q
  -/
  exact (HPQ HP)
end

In fact, for proofs of the form begin exact X, end there is no point entering tactic mode at all:

try it!

example (P Q : Prop) (HP : P) (HPQ : P → Q) : Q := HPQ HP