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 →

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).