## Stream: new members

### Topic: factorise (?) quantifier in a goal

#### Alice (Nov 14 2020 at 10:45):

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 (Nov 14 2020 at 10:50):

Try:

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


#### Johan Commelin (Nov 14 2020 at 10:50):

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

#### Ruben Van de Velde (Nov 14 2020 at 10:51):

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

#### Alice (Nov 14 2020 at 10:58):

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.

Last updated: May 10 2021 at 00:31 UTC