## 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 :=
begin
symmetry at h, exact h,
end


#### tsuki hao (Jul 21 2023 at 07:58):

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

theorem my_lemma4 :
∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
intro x y ε epos ele1 xlt ylt
calc
|x * y| = |x| * |y| := by rw[abs_mul] --绝对值的乘法
_ ≤ |x| * ε := sorry
_ < 1 * ε := sorry
_ = ε := by rw[one_mul]


Does anyone know how this code should be written next?

#### Johan Commelin (Jul 21 2023 at 08:08):

Did you try gcongr?

#### Johan Commelin (Jul 21 2023 at 08:09):

or apply?

#### tsuki hao (Jul 21 2023 at 08:11):

Johan Commelin said:

Did you try gcongr?

gcongr does not apply to this problem, I used apply? but did not get the appropriate tactic

#### Patrick Massot (Jul 21 2023 at 08:11):

Note there are lemmas mentioned in the text right after this exercise.

#### Patrick Massot (Jul 21 2023 at 08:12):

And of course if you are really stuck and simply want the solution then you can find it in the solutions folder.

#### tsuki hao (Jul 21 2023 at 08:12):

Patrick Massot said:

Note there are lemmas mentioned in the text right after this exercise.

Thank you, I only followed the previous part at first!

#### tsuki hao (Jul 21 2023 at 08:13):

Patrick Massot said:

And of course if you are really stuck and simply want the solution then you can find it in the solutions folder.

Can I ask where I can find the 'solutions folder', which may be of great help to my future studies.

#### Patrick Massot (Jul 21 2023 at 08:14):

I'm sorry we have the bad habit of sometimes putting explanations after the exercise statement. We should go through the whole text and systematically fix that. Until we do that you should make sure to check the sentence after each exercise before working on an exercise.

#### Patrick Massot (Jul 21 2023 at 08:15):

If you cloned the repository at https://github.com/leanprover-community/mathematics_in_lean then each chapter folder has a solution subfolder.

#### tsuki hao (Jul 21 2023 at 08:16):

Patrick Massot said:

If you cloned the repository at https://github.com/leanprover-community/mathematics_in_lean then each chapter folder has a solution subfolder.

Thank you, this really helped me a lot!

#### Patrick Massot (Jul 21 2023 at 08:16):

But actually it seems this exercise is missing from the solution file :sad: I'll take a look to understand what happened.

#### tsuki hao (Jul 22 2023 at 02:26):

Patrick Massot said:

Thank you very much!

Last updated: Dec 20 2023 at 11:08 UTC