apply Iff.intro
α : Type
p q : α → Prop
⊢ (∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x
case mp
α : Type
p q : α → Prop
⊢ (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x

case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x