factorise (?) quantifier in a goal

Stream: new members

[Alice]

If i have a goal like : (∀ (n : ℕ), p1(n)) ∧ (∀ (n : ℕ), p2(n)), can i have ∀ (n : ℕ), p1(n) ∧ p2(n)
Or is there a way to intro n in both.

[Ruben Van de Velde]

Try:

example (p q : ℕ → Prop) : (∀ n, p n) ∧ (∀ n, q n) ↔ (∀ n, p n ∧ q n) := by library_search

[Johan Commelin]

split and then intro in both branches. You can avoid repetition using split; intro

[Ruben Van de Velde]

Though Johan's approach is probably simpler; with mine you'd need to do intro and then split after

[Alice]

Yeah but I need the intro to work with hypothesis and I don't want to repeat all that work so I prefer your approach,
library_search give me forall_and_distrib.symm and it's what I want.