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 :=

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?

• Questions on how to use particular tools are off-topic on this StackExchange. StackOverflow would be more appropriate. – Derek Elkins Mar 8 at 0:47
• @DerekElkins We mostly seem to accept questions about Coq, so why not Lean? – David Richerby Mar 8 at 14:29
• @DavidRicherby I don't have a problem with the specific reference to LEAN. (Personally, I'm anti-pseudo-code and would much prefer real code examples as long as they aren't too cluttered.) The problem is that the answer would need to be LEAN-specific. I would view a question like "what tactic do I need to use to perform universal instantiation in Coq" as just as off-topic for the same reasons. If questions like that about Coq aren't being treated as off-topic, that's a failure of community moderation in my mind. – Derek Elkins Mar 8 at 20:38
• @DavidRicherby (contd.) Most of the Coq questions I've seen (and that I would consider on-topic) are really questions about proving things in constructive type theory in general and can and do get answers that are not Coq-specific, e.g. they use some other system such as Agda or just informal type theory. Some LEAN-specific questions would be fine. Questions about LEAN rather than how to use it. For example, "what differences are there between the metatheory implemented by LEAN versus CIC?" – Derek Elkins Mar 8 at 20:38