I'm missing something basic about construction in theorems

Stream: new members

[Matt Pillsbury]

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]

And.intro makes the term. (hp x) ∧ (hq x) is the type. You can't prove a theorem by stating the theorem.

[Kevin Buzzard]

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]

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]

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!