issues extracting proofs

Stream: lean4

[Arien Malec]

Working through TPIL4, and where I was able to extract proofs to subproofs for the props chapter, I'm having typing issues for the quantifiers chapter.

here's a super simple example:

variable (α : Type) (p q : α → Prop)

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

example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
  Iff.intro (fun h => all_and_separable_quantifiers h)
    -- (fun (h: ∀ x, p x ∧ q x) =>
    --   have hp: (∀ x, p x) := fun y => (h y).left
    --   have hq: (∀ x, q x) := fun y => (h y).right
    --   ⟨hp,hq⟩
    -- )
    (fun (h: (∀ x, p x) ∧ (∀ x, q x)) =>
      fun y => show p y ∧ q y from And.intro (h.left y) (h.right y))

the typing issue is:

application type mismatch
  all_and_separable_quantifiers h
argument
  h
has type
  ∀ (x : α), p x ∧ q x : Prop
but is expected to have type
  Type : Type 1

If I pointsfree the subproof call, I get instead

application type mismatch
  Iff.intro all_and_separable_quantifiers
argument
  all_and_separable_quantifiers
has type
  ∀ (α : Type) (p q : α → Prop), (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x : Prop
but is expected to have type
  (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x : Prop

lean4 seems to be interpreting the types in the variable statement differently between thoerem and example or is there some obvious typo I'm missing?

[Rish Vaishnav]

Your variables (α : Type) (p q : α → Prop) are not implicit, so all_and_separable_quantifiers expects them to be explicitly given as your first arguments. Try:

variable {α : Type} {p q : α → Prop}

[Arien Malec]

Thanks -- I see now I previously explicitly declared implicit parameters in my code for the props chapter.