d / 2 < a implies d < 2 * a

Stream: Is there code for X?

[Michael Stoll]

Is there really no substantially easier way to get the following?

import Mathlib.Tactic

open Nat in
lemma lt_two_mul_of_div_two_lt {a d : ℕ} (h : d / 2 < a) : d < 2 * a := by
  rw [lt_iff_add_one_le, ← div_add_mod d 2, add_right_comm]
  rw [lt_iff_add_one_le, ← mul_le_mul_left (a := 2) zero_lt_two] at h
  rw [mul_add, two_mul 1, ← add_assoc] at h
  exact (add_le_add_left (lt_succ.mp <| mod_lt d (zero_lt_two)) _).trans h

[Eric Wieser]

import Mathlib.Tactic

open Nat in
lemma lt_two_mul_of_div_two_lt {a d : ℕ} (h : d / 2 < a) : d < 2 * a := by
  rwa [Nat.div_lt_iff_lt_mul two_pos, mul_comm] at h

[Michael Stoll]

open Nat in
lemma lt_two_mul_of_div_two_lt {a d : ℕ} (h : d / 2 < a) : d < 2 * a := by
  rwa [Nat.div_lt_iff_lt_mul zero_lt_two, mul_comm] at h

[Ruben Van de Velde]

import Mathlib.Tactic

open Nat in
lemma lt_two_mul_of_div_two_lt {a d : ℕ} (h : d / 2 < a) : d < 2 * a := by
  rw [mul_comm]
  apply Nat.lt_mul_of_div_lt h
  norm_num

[Ruben Van de Velde]

:racecar::racecar::racecar:

[Michael Stoll]

apply? doesn't seem to give anything helpful here...

[Ruben Van de Velde]

I'm guessing all of us figured out what the name should be

[Michael Stoll]

But

open Nat in
lemma lt_two_mul_of_div_two_lt {a d : ℕ} (h : d / 2 < a) : d < 2 * a := by
  rw [mul_comm]
  apply?

does.

[Michael Stoll]

So you have to know that a * 2 is better than 2 * a.

[Eric Wieser]

The argument for why it's better is that you'd expect it to hold even in the non-commutative case

[Kevin Buzzard]

lemma lt_two_mul_of_div_two_lt {a d : ℕ} (h : d / 2 < a) : d < 2 * a := by omega

(except this only works in a few months' time...)

[Jireh Loreaux]

as long as it works in a few months time and omega isn't working on it for a few months time like in Lean 3 :laughing:

[Michael Stoll]

Eric Wieser said:

The argument for why it's better is that you'd expect it to hold even in the non-commutative case

But with natural numbers and integers, writing 2* a is much more common than a * 2...

[Eric Wieser]

Sure, but docs#Nat.div_lt_iff_lt_mul isn't about a * 2, it's about a * b

[Michael Stoll]

So the problem is that specializing may change the preferred spelling and thus make the general lemma hard to find.
Would it make sense to add the version with k * y somewhere in Mathlib?

[Eric Wieser]

I'm not convinced: you can find the lemma easily by searching for div_lt_iff, which rw_search might be able to find for you

[Michael Stoll]

Did rw_search hit Mathlib? It doesn't seem to work for me (after updating Mathlib).

[Jireh Loreaux]

It's not merged yet, no.