How to remove a universal quantifier in Lean theorem prover I am working with two binary relations: g_o and pw_o, and I've defined pw_o below:

constants {A : Type} (g_o : A → A → Prop)

def pw_o (x y : A) : Prop := ∀ w : A, (g_o w x → g_o w y) ∧ (g_o y w → g_o x w)

I need to prove the following:

theorem prelim: ∀ x y z : A, g_o x y ∧ pw_o y z → g_o x z :=

I start with these tactics:

begin

   intros,

   cases a with h1 h2,

end


And I have this:

x y z : A,
h1 : g_o x y,
h2 : pw_o y z
⊢ g_o x z


Since pw_o is defined with a universal quantifier, I'd like to substitute w with x, then I would have (g_o x y → g_o x z) ∧ (g_o z x → g_o y x). After isolating the first conjunct with the "cases" tactic, I can use modus ponens on that first conjunct and h1. 
How can I tell Lean to replace w in the definition of pw_o with x and replace x and y in the definition of pw_o with y and z, respectively?
I've found an answer to the question I've posed. Here are the tactics I've used:

begin
   unfold pw_o,
   intros,
   cases a with h1 h2,
   let h3 : A := x,
   let h4 : (g_o x y → g_o x z) ∧ (g_o z x → g_o y x) := h2 x,
   apply (h4.left h1),
end


I've unfolded pw_o to make the universal quantifier explicit. After I've isolated pw_o y z as a hypothesis, I've replaced all occurrences of w with x. Since h4.left is a function from g_o x y to g_o x z, I've applied it to h1, which is a term of g_o x y, to obtain a term of g_o x z, which was the ultimate goal.