Exercise with universal quantifier

Stream: lean4

[Isabel Dahlgren]

Here's my attempt at the first problem from section 4 in Theorem Proving in Lean 4, using tactic mode.

example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := by
  apply Iff.intro
  . intro h
    sorry
  . intro h
    sorry

When I replace sorry by intro y, I get "tactic 'introN' failed, insufficient number of binders
". Any hints on how to proceed? Thanks. :pray:

[Yaël Dillies]

Use constructor

[Yaël Dillies]

The goal at this point is not a forall. It's something ∧ something_else, so it doesn't make sense to introduce a variable.

[Isabel Dahlgren]

That did it, thanks! :ok:

[Kevin Buzzard]

@Isabel Dahlgren When I was just starting out I made a tactic cheat sheet saying things like "if the goal is P ∧ Q then use constructor, and if you want to use a hypothesis h : P ∧ Q then do cases' h with hP hQ (and then a fair few more lines with other common Lean things like P → Q or ∃ x, P x etc).

[Martin Dvořák]

Lean 4 version: https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf