I'm learning to use the LEAN theorem prover and I got stuck in a proof of a simple fact in first-order logic:$$ p(x) \rightarrow \forall x p(x) $$My code is the following:variables (A : Type) (p q : A  Prop)example (x : A) : p x  ( x, p x) :=assume H : p x,take x : A,show p x, from Hbut it keeps saying that H has type p x_1, instead of what I expected, which is type p x.
What's wrong with this LEAN proof?
lo.logic;type theory;coq
Your example is not true, that's why you cannot prove it. If we assume your example is true (which we do using the sorry tactic), then we can prove false. The proof goes as follows. We first pick x to be 0 and p to be the property that a number n is equal to 0. So p x is p 0 is 0 == 0 which is obviously true. Your example now provides us with the proof that p holds for all numbers. We pick 1, which is a contradiction because 0 <> 1.variables (A : Type) (p : A  Prop)lemma lma (x : A) : p x  ( x', p x') :=  assume H : p x,  take x' : A,  sorrylemma inconsistent : false :=  assert h : 0 == 0  ( x, x == 0), from (lma num ( n, n==0) 0),  assert e : 1 == 0, begin    refine (h _ 1),     reflexivity  end,  show false, by cases eThe formula that you posted is also false in first order logic, even  x, p x  ( x, p x) is not a true statement. Note that your example is different from the true statement ( x, p x)  ( x, p x).The error message that you see stems from the fact that you are trying to use the hypothesis p x where the hypothesis p x' is expected (you are confusing the xes)