How to remove a universal quantifier in Lean theorem prover
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.