Distributing Existential Qualification over Disjunction

Stream: Is there code for X?

[Sophia C]

I'm working on a proof, and I managed to get to a state where I have (p : ℕ -> Prop) and (q : ℕ -> Prop) in scope and ∃ n, p n ∨ q n Is there a tactic / function I can use to convert this goal into something of the form ∃ n, p n ∨ ∃ n, q n? Or is that not possible?

[Felix Weilacher]

docs#exists_or