That is also true, but its proof is different. Proofs have types; the "and.intro hq hp" part has type "q /\ p". If you change it to "and.intro hp hp", you can prove "p /\ p". That is, the following works:

    theorem and_commutative (p q : Prop) : p ∧ q → p ∧ p :=
    assume hpq : p ∧ q,
    have hp : p, from and.left hpq,
    have hq : q, from and.right hpq,
    show p ∧ p, from and.intro hp hp

(and then you should rename it from "and_commutative" to something else, and you can remove the "hq" line)

Just for the sake of comparison, the same proof in Coq might be written:

    Theorem and_commutative (P Q : Prop) : P ∧ Q → Q ∧ P.
    Proof.
      intros [HP HQ].
      split.
        - apply HQ.
        - apply HP. 
    Qed.

"intros [HP HQ]" separates the two conjuncts of the hypothesis into separate hypotheses (P, and Q); "split" breaks the goal (Q ∧ P) into two subgoals (Q, and P), and the two applications prove the two subgoals.

It could also be written:

    Theorem and_commutative_2 (P Q : Prop) : P ∧ Q → Q ∧ P.
    Proof. tauto. Qed.

...as the proof tactic "tauto" is capable of proving this (simple) theorem immediately.

There are tons of other ways of writing the same thing in Lean too, of course. Here is one:

    theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
    begin intros, simp * end

https://leanprover.github.io/live/3.4.1/#code=theorem%20and_...

In Lean you could do

  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := by cc

for a tactic proof and

  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := λ ⟨h,j⟩,⟨j,h⟩

for a term proof (just write down the function).

Cool, thanks for this. I've yet to play with Lean, but it looks very interesting! (I'm hoping that my time invested in Coq will transfer reasonably well...)

You're welcome! I'm in a similar boat, coming to this tutorial from a Coq background (and some Isabelle/HOL). I'm pleasantly surprised how similar many things are. But I'm also a bit disappointed because I was under the impression that Lean was relying on automation via Z3 a lot more. Not quite done with the tutorial yet, so there might still be some material to this effect coming up, but I'm afraid not.