# Zulip Chat Archive

## Stream: new members

### Topic: I'm missing something basic about construction in theorems

#### Matt Pillsbury (Dec 04 2022 at 00:57):

I tripped over an error message as I've been working my way through the exercises in *Theorem Proving in Lean 4*. This simple attempt at a proof...

```
variable (α : Type) (p q : α → Prop)
example : (∀ x, p x) ∧ (∀ x, q x) → (∀ x, p x ∧ q x) :=
(fun ⟨hp, hq⟩ =>
fun x => (hp x) ∧ (hq x))
```

...gives me this error message that I'm very puzzled by:

```
application type mismatch
And (_ : p x)
argument
hp x
has type p x : Prop
but is expected to have type Prop : Type
```

However, this seemingly equivalent approach works:

```
#check And.intro -- And.intro : ?m.21 → ?m.22 → ?m.21 ∧ ?m.22
example : (∀ x, p x) ∧ (∀ x, q x) → (∀ x, p x ∧ q x) :=
(fun ⟨hp, hq⟩ =>
fun x => And.intro (hp x) (hq x))
```

Where is the difference in the two proofs that breaks the first one?

#### Kevin Buzzard (Dec 04 2022 at 01:00):

`And.intro`

makes the term. `(hp x) ∧ (hq x)`

is the type. You can't prove a theorem by *stating* the theorem.

#### Kevin Buzzard (Dec 04 2022 at 01:02):

In fact `(hp x) ∧ (hq x)`

is just a mess. If `P`

and `Q`

have type `Prop`

then `P ∧ Q`

has type `Prop`

and it's the theorem statement. `hp x`

is a proof, so it has type `P`

for some `P`

of type `Prop`

. You're confusing types and terms.

#### Kevin Buzzard (Dec 04 2022 at 01:03):

`def foo := 2 + 2 = 5`

. Do you understand what that means and why it works? I ask because I was confused about this when I was a beginner. Another example is `def f := Nat -> Nat`

.

#### Matt Pillsbury (Dec 04 2022 at 01:27):

I think I get it now, especially based on the last bit. I was confusing the **type** of `And.intro`

with the **term** `And.intro`

.

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC