## Conjunction

To build a proof of $A \land B$, we needs proofs of $A$ and $B$. In Lean, this is accomplished by `And.intro`

.

For elimination, we use `And.left`

and `And.right`

to extract proofs from `A ∧ B`

.

## Disjunction

For the or-introduction rules, we have

For $\lor$-elimination we need

three things :

- $A \lor B$
- A proof $A \vdash C$
- A proof $B \vdash C$ Let’s see what it looks like in Lean.

So to use `Or.elim`

we need three proofs:

`r : A ∨ B`

`p : A → C`

`q : B → C`

Let’s see a one direction of a commutativity of `∨`

in Lean and at the same time get some sense of how to build up a proof in steps. Often Lean can “fill in” arguments from the context. You can ask it by placing a `_`

. Let’s see what happens here.

The infoview might look something like

Lean is asking for our proofs of `B → B ∨ A`

and `A → B ∨ A`

. Remember that the are functions that turn any proof of `B`

into a proof of `B ∨ A`

and the same with `A`

to `B ∨ A`

. We can fill in the proof by providing such functions using or eliminations.

## Bi-implication

We can eliminate a bi-implication into two implications.

Here `mp`

stands for “Modus ponens” and `mpr`

for the “reverse”.

To introduce a bi-implication, we need proofs of `A → B`

and `B → A`

.