apply

You can use apply H if you have a hypothesis H : P → Q and your goal is Q. It changes the goal to P.

...
H : P → Q,
...
⊢ Q

becomes

...
H : P → Q,
...
⊢ P

after apply H.

In maths, what is happening is that if you know that P implies Q then to prove Q it suffices to prove P.

Example (¬)

try it!

theorem contrapositive (P Q : Prop) (HPQ : P → Q) : ¬ Q → ¬ P :=
begin
/-
  P Q : Prop,
  HPQ : P → Q
  ⊢ ¬Q → ¬P
-/
  intro HnQ,
  intro HP,
/-
  P Q : Prop,
  HPQ : P → Q,
  HnQ : ¬Q,
  HP : P
  ⊢ false
-/
  apply HnQ, -- !
/-
  P Q : Prop,
  HPQ : P → Q,
  HnQ : ¬Q,
  HP : P
  ⊢ Q
-/
  apply HPQ,
  assumption
end

Above is a proof of the fact that if \(P\implies Q\) then \(\lnot Q\implies \lnot P\) in Lean. A mathematician might say “Let’s prove this by contradiction”, and then might feel bound to the idea that the last line of their proof must be ”...but this is a contradiction, and hence we are done”. But mathematics is more flexible than this. After assuming \(P\implies Q\) and \(\lnot Q\) and \(P\) our goal is now to prove false, which in practice means that we need to derive a contradiction from our assumptions. However our hypothesis \(\lnot Q\) can be interpreted as Q → false, and using the apply tactic reduces the goal from false to Q, reducing our problem to proving Q from P and P → Q; all of a sudden we are not proving something by contradiction any more.