Where should I add this lemma?

Stream: mathlib4

[Evangelos Kitsios]

Hello and sorry if this question is a bit trivial but this is my first time contributing on mathlib.

I have the following lemma that I believe would be a nice addition in mathlib.
le_of_dvd_abs {x y : ℤ} (h₁ : y ≠ 0) (h₂ : x ∣ y) : x ≤ |y|

The issue is that I do not know the exact file where I should add the said lemma. I tried adding it to the same file as "Int.le_of_dvd" but this file does not seem to be inside the repository
Any suggestion is welcome. Thank you.

[Violeta Hernández]

I'm not confident that we should have this, given we can just prove it as:

import Mathlib.Algebra.Order.Ring.Abs

theorem le_of_dvd_abs {x y : ℤ} (h₁ : y ≠ 0) (h₂ : x ∣ y) : x ≤ |y| :=
  Int.le_of_dvd (abs_pos.2 h₁) ((dvd_abs ..).2 h₂)

[Evangelos Kitsios]

Indeed it is not a hard lemma to prove by itself, but isn't this the case with many other lemmas inside mathlib? It seems to me that it is intuitive enough to exist as a standalone theorem.

[Johan Commelin]

Can you find some proofs in mathlib that would be simplified using this lemma? That would be good evidence to include it.

[Patrick Massot]

Is this proof found by your standard automation (say grind and aesop)? I think such obvious looking statements should either be in mathlib or deduced automatically from lemmas in mathlib.

[Evangelos Kitsios]

I did try various automation tactics but none of them were successful.

[Jovan Gerbscheid]

Either way I think it should be called le_abs_of_dvd.

[Chris Henson]

This works too (found with aesop):

import Mathlib.Algebra.Order.Ring.Abs

theorem le_of_dvd_abs {x y : ℤ} (h₁ : y ≠ 0) (h₂ : x ∣ y) : x ≤ |y| := by
  simp_all [Int.le_of_dvd]

[Kim Morrison]

I think we could add this. We don't have great automation yet for divisibility+orders.

[Kim Morrison]

The theorem name is incorrect, though, surely le_abs_of_dvd?

[Evangelos Kitsios]

In that case, which file would be the appropriate one for this to be added?

[Ruben Van de Velde]

Mathlib.Algebra.Order.Ring.Abs sounds reasonable