## Stream: new members

### Topic: inequality

#### Alexandre Rademaker (May 30 2020 at 22:03):

I was expecting to learn how to prove example {x y : ℕ} {h : x + 1 = y + 2} : x > y := sorry from NNG but it looks like NNG defines > differently from the Lean 3 standard library. Any idea?

#### Chris Hughes (May 30 2020 at 22:24):

by omega or by linarith should work.

#### Alexandre Rademaker (May 30 2020 at 22:28):

hum, not directly, and both are in mathlib, right?

#### Jalex Stark (May 30 2020 at 22:42):

why are you asking about mathlib? did you try one of those proofs and it told you it couldn't find the name?

yes. Lean 3.

#### Jalex Stark (May 30 2020 at 22:44):

are you able to import anything from mathlib?

#### Jalex Stark (May 30 2020 at 22:44):

are you in a project where you installed mathlib using leanproject?

#### Alexandre Rademaker (May 30 2020 at 22:45):

no, I am trying to prove without mathlib, only using Lean 3 standard definitions.

#### Jalex Stark (May 30 2020 at 22:46):

oh, okay, I think that was not clear

#### Jalex Stark (May 30 2020 at 22:46):

well you could start by unfolding the definition of <

#### Jalex Stark (May 30 2020 at 22:46):

the NNG-style proof would probably be an induction

#### Jalex Stark (May 30 2020 at 22:47):

(I don't know why anyone would want to do math in lean without mathlib; if you give more context maybe we can be more helpful)

#### Kevin Buzzard (May 30 2020 at 22:51):

I probably don't use > at all in NNG -- all the lemmas are for < and <=. I can believe I defined it differently -- I played around with several definitions and tested them on undergraduates before deciding which one to go with. You can just switch notation off and unfold if you want to see the definition you're playing with.

#### Kevin Buzzard (May 30 2020 at 22:52):

But there will probably be a lemma of the form y < x iff y+1 le x and then another one saying you can cancel +1 in an inequality. These both sound like natural lemmas so they'll be in...oh, they might be in mathlib. I have no idea what's in core lean. Core lean wasn't designed for this kind of question

#### Jalex Stark (May 30 2020 at 22:53):

in fact we're doing our best to take math out of core lean

#### Alexandre Rademaker (May 30 2020 at 22:54):

@Jalex Stark The example looks very simple and my goal is to understand the details. surely mathlb provides tactics like omega and linarith but I want to explore the basics here. Actually, the example came from a very simple exercise that I am trying to show how to formalize in Lean. See the balances in https://www.youtube.com/watch?v=4JpFWfkAtHY&t=2088s (video in Portuguese).

#### Jalex Stark (May 30 2020 at 22:55):

sure, I think it's fine to not want to use a high-powered tactic for this

#### Jalex Stark (May 30 2020 at 22:55):

but not using mathlib is silly

#### Kevin Buzzard (May 30 2020 at 22:55):

If you don't import data.nat.basic from mathlib then you will probably be missing a bunch of random lemmas though

#### Kevin Buzzard (May 30 2020 at 22:55):

So you might end up having to reprove them all by induction

#### Kevin Buzzard (May 30 2020 at 22:58):

Files like data.nat.basic used to be in core lean before they dumped the maths out into mathlib

#### Kevin Buzzard (May 30 2020 at 23:03):

open nat

example {x y : ℕ} {h : x + 1 = y + 2} : x > y :=
begin
apply nat.lt_of_succ_le,
rw h,
end


#### Kevin Buzzard (May 30 2020 at 23:03):

Enough of what I wanted was in core

#### Kevin Buzzard (May 30 2020 at 23:06):

I use the fact that y>x is definitionally x<y

#### Alexandre Rademaker (May 30 2020 at 23:15):

Jalex Stark said:

but not using mathlib is silly

sure, if my goal was something more complex and I had some inequalities on my way.. I can understand the value of mathlib. But that is not the case, it is much more basic stuff that I want to explore.

#### Jalex Stark (May 30 2020 at 23:23):

i still don't really understand your goals. what if core lean literally didn't have a definition of the natural numbers? would you still want to avoid mathlib?

#### Alexandre Rademaker (May 31 2020 at 00:07):

thank you @Kevin Buzzard, clear and direct solution as always! ;-)

#### Alexandre Rademaker (May 31 2020 at 00:15):

No @Jalex Stark, it is all about the level of abstraction I am focusing on? If Lean didn't have any natural numbers definitions, I guess for that particular problem I would not be able to avoid mathlib. It is not very different from programming and when we believe that it is worth to depend on a library or not. But you are right I should start using mathlib to have also a clue about what it can provide.

(deleted)

#### Alexandre Rademaker (May 31 2020 at 00:36):

Kevin Buzzard said:

I use the fact that y>x is definitionally x<y

Where is that?

#### Bryan Gin-ge Chen (May 31 2020 at 00:39):

I think Kevin just means that he proves x < y and Lean accepts it as a proof of y > x.

#### Alexandre Rademaker (May 31 2020 at 00:55):

I found in the core.lean

@[reducible] def gt {α : Type u} [has_lt α] (a b : α) : Prop := has_lt.lt b a
...
infix >        := gt


maybe this is the definition of y > x as gt y x := has_lt.lt y x

#### Jalex Stark (May 31 2020 at 01:04):

thanks, I think I understand your goal now. probably you want to look at the proofs of the lemmas that kevin invoked in his proof?

#### Jalex Stark (May 31 2020 at 01:05):

in mathlib we just try to avoid using > in our theorem statements as much as posisble

#### Michael Beeson (Jul 13 2020 at 06:24):

How can I get a \neq p in a hypothesis h (or a goal for that matter) rewritten as p \neq a?

#### Kenny Lau (Jul 13 2020 at 06:24):

replace h := h.symm

#### Kenny Lau (Jul 13 2020 at 06:24):

apply ne.symm

#### Michael Beeson (Jul 13 2020 at 06:25):

ah. I tried among other things neq.sym.... Thank you

#### Kenny Lau (Jul 13 2020 at 06:26):

this reminds me to PR the list of names of symbols

#### Kenny Lau (Jul 13 2020 at 06:32):

https://github.com/leanprover-community/leanprover-community.github.io/pull/93

#### Jalex Stark (Jul 13 2020 at 11:23):

example (a b : ℕ) (h : a ≠ b) : b ≠ a :=