How to use proofs from Lean's standard library.

Stream: new members

[newptcai]

I read in Theorem Proving in Lean 4 that

Lean's standard library contains proofs of many valid statements of propositional logic, all of which you are free to use in proofs of your own.

But I could not find anywhere of how to use any of the proofs listed in the document. Can anyone help me find how to use, say something like
p ∧ q ↔ q ∧ p?

[Martin Dvořák]

If you have a lemma foo : bar ↔ baz you will typically use it as rw [foo] or similar.

[Kyle Miller]

docs#and_comm is a ∧ b ↔ b ∧ a

[Kyle Miller]

(I guess this one is in the std4 library rather than Lean 4 itself. If you are using mathlib, then you definitely have and_comm.)

[newptcai]

Kyle Miller said:

docs#and_comm is a ∧ b ↔ b ∧ a

Thanks. But how can I load it in my .lean file?

[Kyle Miller]

Have you done any exercises yet? (Do you have a working Lean environment?)

[Martin Dvořák]

First, show us your lakefile.lean.

[Sebastian Ullrich]

And.comm does not have to be imported

[Patrick Massot]

Kyle, you're referring to Lean 3 here.

[Patrick Massot]

The question is explicitly about Lean 4.

[newptcai]

I am doing the exercise at the end of this page
Here's my code.

variable (p q r : Prop)

theorem and_comm : p ∧ q → q ∧ p :=
  (fun h: p ∧ q =>
      have hp : p := h.left
      have hq : q := h.right
      ⟨hq, hp⟩)

-- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p :=
  Iff.intro
    (and_comm p q)
    (and_comm q p)

I was just wonder if this has already been implemented in Lean so I can use directly.

[Kyle Miller]

(@Patrick Massot the docs linkifier is for the mathlib4 docs now)

[Patrick Massot]

Oh right, I need to get used to this.

[Kyle Miller]

@newptcai Sebastian pointed out that docs#And.comm should be available to you

[newptcai]

Thank you all. This seems to work

example : p ∧ q ↔ q ∧ p := And.comm

[Alexander Lucas]

[redacted] (sorry about that)