If the goal is ⊢ X then exact hp will close the goal if and only if hp : X

theorem not_not_intro (P : Prop) :
  P → ¬¬ P :=
begin
  intro hp,
  apply not.intro,
  intro hnp,
  apply hnp,
  exact hp,
end

intro hp will turn a goal ⊢ P → Q into a hypothesis hp : P and goal ⊢ Q. If P and Q are sets intro p means “let p be an arbitrary element of P”. If P and Q are propositions then intro hp says “assume P is true” (i.e. “let hp be a proof of P). We also use intro to prove a universally quantified statement.

theorem forall_impl 
(A B : U → Prop) : (∀ x, A x → B x) → (∀ x, A x) → (∀ x, B x) := 
begin 
  intro h, 
  intro u, 
  intro a, 
  have e, from u a,    
  have h_a, from h a, 
  show B a, from h_a e,   
  -- exact h_a e,  
end  

If you have h : P → Q and your goal is ⊢ Q then apply h changes the goal to ⊢ P. If you are trying to create a proof of Q, and h is a rule which turns proofs of P into proofs of Q, then it will suffice to construct a proof of P. It is the bottom-to-top version of application. Here’s an example:

theorem curry (P Q R : Prop) : (P ∧ Q → R) → (P → (Q → R) :=
begin 
intro h,
intro hp, 
intro hq, 
apply h,  
constructor, 
exact hp, 
exact hq,
end

Puzzle: figure out what constructor does by examining what Lean tells you about your goals.

refl proves goals of the form t = t, and more generally goals of the form t ~ t where ~ is any reflexive binary relation.

example (a b c d : ℕ) : (a + b) * (c + d) = (a + b) * (c + d) := 
begin 
refl, 
end

The rw tactic corresponds to the substitution rule of equality which we discussed in the lecture on the equality predicate. If h is a proof of A = B (i.e. h : x = y), then rw h will change all xs in the goal to ys. Variants: rw ←h (get the backward arrow with \l) changes y to x and rw h at u (changes x to y in hypothesis u instead of the goal). Here is an example:

example (m n : ℕ) (h : n = m + 6) : 2 * n = 2 * (m + 6) :=
begin 
rw h, 
end 

Here is another example:

example (P Q : Prop) (h : P ↔ ¬ Q) : (P → ¬ ¬ P) → (¬ Q → ¬ ¬ ¬  Q) := 
begin
  rw ← h, 
  intro u, 
  exact u, 
end  

Note that here Lean uses propositional extensionality to equate two equivalent proposition.

#check propext

This tactic has several variants and it is used quite frequently. In its most basic form, simp will try to use relevant lemmas and hypotheses to simplify the goal. dsimp is similar to simp, except that it only uses definitional equalities. See here for a full guide for all usages of simp.

example : ∀ n : ℕ,  2 ≠ 2 * 2 * n := begin
  intro n, 
  cases n with d hd,
  simp, 
  rw nat.succ_eq_add_one, 
  linarith, 
end

and

example (n : ℕ) (h : n + 1 - 1 ≠ 0) : n + 1 ≠ 1 :=
begin
  simpa using h,
end