h: x < y, prove 2*x < 2*y

Stream: new members

[Adam Robinson]

Hello! I am new here and now to Lean. I have a question, am I at the right place/room to ask? :)

[Adam Robinson]

new to Lean*

[Kevin Buzzard]

(deleted)

[Adam Robinson]

I am stuck at circular or contradictory conclusions when I try to solve

import data.nat.basic
open nat

lemma learning ( x y : ℕ ) (x < y): 2*x < 2*y :=
begin

end
/-
rw lt_iff_exists_add at H,
  cases H with x h,
  cases h with y h,
  rw lt_iff_exists_add,
  use x,
  split,
  apply y,
  simp,
  ---??
-/

[Adam Robinson]

I also tried 'mul_lt_mul_left', but it did not change ca < cb into a < b

[Kevin Buzzard]

Edit your first message and enclose the code in two lines just containing three backticks ``` . Right now markup is eating things like your multiplications so it's hard to read and hence to answer. Read the information at #mwe for more hints on how to ask a good question.

[Notification Bot]

A message was moved here from #new members > finite by Adam Robinson.

[Adam Robinson]

Thanks for the pointers. I'll edit my message and make the code readable.

[Kevin Buzzard]

The first problem is that you have a typo in your question: you are asking about 2x<2y but your code has 2x<2x so it's not provable. Secondly I wouldn't recommend cases H with x h because then you'll have two variables both called x which is a recipe for disaster. Thirdly (x < y) isn't correct syntax -- this hypothesis needs a name (or else you'll end up with three variables called x). Try (H : x < y). Has that got you on the right track?

[Adam Robinson]

I made some errors :/ Thanks

[Adam Robinson]

I have made some more changes and I am still stuck at lemmas I cannot prove:

import data.nat.factorial.basic -- imported because this lemma is a simpler version of my actual problem.
import data.nat.basic
open nat

lemma t ( x y : ℕ ) ( H: x < y ): 2*x < 2*y :=
begin

end

/-
rw lt_iff_exists_add,
use 1,
split,
-/

[Kevin Buzzard]

If you're going to use lt_iff_exists_add (which will work) then what is the rest of the maths proof? Lean will not come up with proofs by itself (unless you use the AI interface, which is flaky at best), it will just check your proofs.

[Eric Wieser]

which will work

Though use 1 is not going to do you any favors

[Kevin Buzzard]

(that's why I asked about the maths proof)