{ intro h
  apply And.intro
  { intro x
    apply And.left
    apply h }
  { intro x
    apply And.right
    apply h } }
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
case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x