# 2.3 Conjunction

Conjunction represents "and". A proof of `P ∧ Q` contains two pieces of evidence: a proof of `P` and a proof of `Q`. In Lean, conjunction behaves like a pair whose fields are logical proofs.

## Problem

You want to prove or use a statement of the form:

```lean
P ∧ Q
```

To prove it, you must prove both sides. To use it, you may extract either side.

## Solution

Use `constructor` to split a conjunction goal into two goals.

```lean
theorem make_conjunction (P Q : Prop) : P -> Q -> P ∧ Q := by
  intro hp
  intro hq
  constructor
  · exact hp
  · exact hq
```

After `constructor`, Lean creates two goals:

```lean
⊢ P
⊢ Q
```

Each goal is solved using the corresponding hypothesis.

## Extracting the Left and Right Sides

If you have:

```lean
h : P ∧ Q
```

then `h.left` is a proof of `P`, and `h.right` is a proof of `Q`.

```lean
theorem conjunction_left (P Q : Prop) : P ∧ Q -> P := by
  intro h
  exact h.left

theorem conjunction_right (P Q : Prop) : P ∧ Q -> Q := by
  intro h
  exact h.right
```

These projections are the most direct way to use a conjunction.

## Case Analysis on a Conjunction

You can also decompose a conjunction with `cases`.

```lean
theorem conjunction_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  cases h with
  | intro hp hq =>
    constructor
    · exact hq
    · exact hp
```

The command `cases h` replaces the conjunction proof with its two components:

```lean
hp : P
hq : Q
```

Then the goal `Q ∧ P` is proved by constructing both parts in reverse order.

## Term Form

The same proof can be written without tactics.

```lean
theorem conjunction_swap_term (P Q : Prop) : P ∧ Q -> Q ∧ P :=
  fun h => And.intro h.right h.left
```

The constructor `And.intro` takes a proof of the left side and a proof of the right side.

Its shape is:

```lean
And.intro : P -> Q -> P ∧ Q
```

So to build `Q ∧ P`, we pass `h.right : Q` first and `h.left : P` second.

## Nested Conjunctions

Conjunctions associate to the right only according to the syntax you write. The propositions below are different shapes:

```lean
(P ∧ Q) ∧ R
P ∧ (Q ∧ R)
```

They contain the same logical information, but the proof objects are nested differently.

```lean
theorem reassociate_conjunction
    (P Q R : Prop) :
    (P ∧ Q) ∧ R -> P ∧ (Q ∧ R) := by
  intro h
  constructor
  · exact h.left.left
  · constructor
    · exact h.left.right
    · exact h.right
```

The hypothesis has type:

```lean
h : (P ∧ Q) ∧ R
```

So:

```lean
h.left       : P ∧ Q
h.left.left  : P
h.left.right : Q
h.right      : R
```

The proof rebuilds the conjunction in the requested shape.

## Building Conjunctions Step by Step

Sometimes it is clearer to name intermediate proofs.

```lean
theorem conjunction_with_have
    (P Q R : Prop)
    (hp : P)
    (hq : Q)
    (hr : R) :
    P ∧ (Q ∧ R) := by
  have hqr : Q ∧ R := by
    constructor
    · exact hq
    · exact hr
  constructor
  · exact hp
  · exact hqr
```

This style is useful when one side of the conjunction is itself a nontrivial proof.

## Using Pattern Matching in `intro`

Lean can destruct a conjunction as soon as it is introduced.

```lean
theorem conjunction_swap_intro_pattern
    (P Q : Prop) :
    P ∧ Q -> Q ∧ P := by
  intro ⟨hp, hq⟩
  exact ⟨hq, hp⟩
```

The notation:

```lean
⟨hp, hq⟩
```

means that the proof of `P ∧ Q` is decomposed into its two components.

The same notation can also construct conjunctions:

```lean
⟨hq, hp⟩
```

constructs a proof of `Q ∧ P`.

## Conjunction and `simp`

Simple conjunction projections are often solved by `simp`.

```lean
theorem simp_conjunction_left (P Q : Prop) : P ∧ Q -> P := by
  intro h
  simp [h]

theorem simp_conjunction_comm (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  constructor
  · exact h.right
  · exact h.left
```

For beginner code, prefer explicit projections or `cases`. They show the proof shape clearly.

## Common Patterns

To prove:

```lean
⊢ P ∧ Q
```

use:

```lean
constructor
```

and prove both goals.

To use:

```lean
h : P ∧ Q
```

use:

```lean
h.left
h.right
```

or:

```lean
cases h with
| intro hp hq => ...
```

To build a conjunction directly, use:

```lean
exact ⟨hp, hq⟩
```

## Common Pitfalls

Do not treat `h : P ∧ Q` as two hypotheses until you extract them. Lean sees one hypothesis whose type is a conjunction.

Do not reverse the order when constructing a conjunction. To prove `P ∧ Q`, the first proof must have type `P`, and the second proof must have type `Q`.

Do not assume nested conjunctions have the same syntactic shape. `P ∧ Q ∧ R` is parsed as `P ∧ (Q ∧ R)`, so projections must follow that structure.

## Takeaway

A conjunction is a pair of proofs. To prove `P ∧ Q`, prove `P` and prove `Q`. To use `P ∧ Q`, extract its left and right components. This pair-like behavior explains `constructor`, `.left`, `.right`, `cases`, and the angle-bracket notation.