Should I open a PR to add these 3 theorems?

Stream: mathlib4

[Yi.Yuan]

import Mathlib

open Nat

lemma div_mul_div {m n k : ℕ} (hn : n > 0) (hkm : m ∣ k) (hkn : n ∣ m) :
    (k / m) * (m / n) = k / n := by
  refine Eq.symm (Nat.div_eq_of_eq_mul_left hn ?_)
  rw [mul_assoc, Nat.div_mul_cancel hkn, Nat.div_mul_cancel hkm]

lemma div_dvd_div {m n k : ℕ} (hn : n > 0) (hkm : m ∣ k) (hkn : n ∣ m) :
    k / m ∣ k / n := by
  use m / n
  exact Eq.symm (div_mul_div hn hkm hkn)

lemma lcm_div_eq {m n k : ℕ} (hm : m > 0) (hn : n > 0) (hkm : m ∣ k) (hkn : n ∣ k) :
    (k / m).lcm (k / n) = k / (m.gcd n) := by
  rw [Nat.lcm_eq_iff]
  exact ⟨div_dvd_div (gcd_pos_of_pos_left n hm) hkm (Nat.gcd_dvd_left m n),
        div_dvd_div (gcd_pos_of_pos_left n hm) hkn (Nat.gcd_dvd_right m n), fun c hmc hnc ↦ by
    rw [Nat.div_dvd_iff_dvd_mul hkm hm] at hmc
    rw [Nat.div_dvd_iff_dvd_mul hkn hn] at hnc
    simpa [Nat.div_dvd_iff_dvd_mul (Nat.dvd_trans (Nat.gcd_dvd_left m n) hkm)
      (gcd_pos_of_pos_left n hm), Nat.gcd_mul_right m c n] using (Nat.dvd_gcd hmc hnc) ⟩

I want to add these three theorems to mathlib. They should belong in Init.Data.Nat.Lemmas and Init.Data.Nat.Dvd, but those files are locked. Where should I put them instead?

[Eric Wieser]

By "locked", what's actually happening is that those files are part of Lean itself

[Eric Wieser]

You can use #find_home to get a suggestion of where to put the lemmas

[Yi.Yuan]

I’ve already tried #find_home, but it didn’t have any useful effect.

[Yi.Yuan]

I’ve opened PR #26488 regarding this issue. Since it’s quite trivial, will someone be reviewing it soon?

[Robin Arnez]

These should surely be in core, if anything..?

[Robin Arnez]

https://github.com/leanprover/lean4 for reference

[Antoine Chambert-Loir]

Note that these lemmas do not require the positivity assumptions:

import Mathlib

open Nat

lemma div_mul_div {m n k : ℕ} (hkm : m ∣ k) (hkn : n ∣ m) :
    (k / m) * (m / n) = k / n := by
  rcases n.eq_zero_or_pos with hn | hn
  · simp [hn]
  refine Eq.symm (Nat.div_eq_of_eq_mul_left hn ?_)
  rw [mul_assoc, Nat.div_mul_cancel hkn, Nat.div_mul_cancel hkm]

lemma div_dvd_div {m n k : ℕ} (hkm : m ∣ k) (hkn : n ∣ m) :
    k / m ∣ k / n := by
  use m / n
  exact Eq.symm (div_mul_div hkm hkn)

lemma lcm_div_eq {m n k : ℕ} (hkm : m ∣ k) (hkn : n ∣ k) :
    (k / m).lcm (k / n) = k / (m.gcd n) := by
  rw [Nat.lcm_eq_iff]
  refine ⟨div_dvd_div hkm (Nat.gcd_dvd_left m n),
        div_dvd_div hkn (Nat.gcd_dvd_right m n), fun c hmc hnc ↦ ?_⟩
  rcases m.eq_zero_or_pos with hm | hm
  · simp [show c = 0 by simpa [hm] using hmc, hmc]
  rcases n.eq_zero_or_pos with hn | hn
  · simp [show c = 0 by simpa [hn] using  hnc, hnc]
  rw [Nat.div_dvd_iff_dvd_mul hkm hm] at hmc
  rw [Nat.div_dvd_iff_dvd_mul hkn hn] at hnc
  simpa [Nat.div_dvd_iff_dvd_mul (Nat.dvd_trans (Nat.gcd_dvd_left m n) hkm)
    (gcd_pos_of_pos_left n hm), Nat.gcd_mul_right m c n] using (Nat.dvd_gcd hmc hnc)

[Yaël Dillies]

Feel free to open a PR and request a review! I can already tell you that those lemmas indeed do not exist, but that your names aren't quite correct. I would expect Nat.div_mul_div_cancel, Nat.div_dvd_div_left, Nat.lcm_div_div_left, and the second one can be gcongr