Zulip Chat Archive

Stream: new members

Topic: factorise (?) quantifier in a goal


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 14 2020 at 10:50):

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

view this post on Zulip 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

view this post on Zulip 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