exists distribution over and

Stream: new members

[Yakov Pechersky]

What's the mathlib name for this lemma and the ones that only retain the left or right branch?

example {α : Type*} {p q : α → Prop} (h : ∃ x, p x ∧ q x) : (∃ x, p x) ∧ (∃ x, q x) :=
exists.elim h (λ x ⟨P, Q⟩, ⟨⟨x, P⟩, ⟨x, Q⟩⟩)

[Kevin Buzzard]

You can probably find it in logic.basic or with library_search but I'm guessing exists_and_distrib. I don't know about the projection ones though

[Mario Carneiro]

the projection ones are just Exists.imp

[Mario Carneiro]

like Exists.imp (\lam _, and.left)