apply And.left
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ p x
case mp.left.self
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ p x ∧ ?mp.left.b

case mp.left.b
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ Prop