Pushing universal quantifier through and

Stream: new members

[Felix Kalker]

Hello all, I would like to know if it is possible to prove the following example in one line:

variables (α : Type*) (p q : α → Prop)

example : (∀ x : α, p x ∧ q x) → ∀ y : α, p y  :=
begin
  intros h y,
  exact (h y).left,
end

Thanks for the help!

[Johan Commelin]

Does the following count:

variables (α : Type*) (p q : α → Prop)

example : (∀ x : α, p x ∧ q x) → ∀ y : α, p y  := assume h y, (h y).left

[Johan Commelin]

Or

import tactic

variables (α : Type*) (p q : α → Prop)

example : (∀ x : α, p x ∧ q x) → ∀ y : α, p y  := by finish

[Andrew Yang]

docs#forall_and_distrib might be useful as well.