# 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?

• 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

## 1 Answer

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.