nightly#131 adaptations for nightly-2025-12-03

Stream: nightly-testing

[Kim Morrison]

chore: adaptations for nightly-2025-12-03 nightly#131

Please review this PR. At the next toolchain release this diff will land in 'master'.

[Kim Morrison]

Hooray, the diff is sane (or at least, only touches 28 files).

[Kevin Buzzard]

These are removed from mathlib with no comment:

theorem cast_mul_floor_div_cancel_of_pos {n : ℤ} (hn : 0 < n) (a : k) : ⌊n * a⌋ / n = ⌊a⌋ := by
  simpa [hn.ne'] using (floor_div_cast_of_nonneg hn.le (↑n * a)).symm

lemma mul_cast_floor_div_cancel_of_pos {n : ℤ} (hn : 0 < n) (a : k) : ⌊a * n⌋ / n = ⌊a⌋ := by
  rw [mul_comm, cast_mul_floor_div_cancel_of_pos hn]

theorem natCast_mul_floor_div_cancel {n : ℕ} (hn : n ≠ 0) (a : k) : ⌊n * a⌋ / n = ⌊a⌋ := by
  simpa using cast_mul_floor_div_cancel_of_pos (n := n) (by lia) a

theorem mul_natCast_floor_div_cancel {n : ℕ} (hn : n ≠ 0) {a : k} : ⌊a * n⌋ / n = ⌊a⌋ := by
  rw [mul_comm, natCast_mul_floor_div_cancel hn]

Can you confirm they found a new home?

[Kim Morrison]

Oh, no, they are not rehomed by me. I thought these just moved from one place to another, but I may have botched the merge here.

[Kim Morrison]

Sorted it out. We're actually okay!

The theorems are not lost - they were generalized:

- cast_mul_floor_div_cancel_of_pos is now in LinearOrderedCommRing (line 271) working for any CommRing R
- natCast_mul_floor_div_cancel is now in LinearOrderedCommRing (line 274)
- mul_cast_floor_div_cancel_of_pos is now in LinearOrderedRing (line 258)
- mul_natCast_floor_div_cancel is now in LinearOrderedRing (line 263)

The PR diff shows deletions because bump/v4.27.0 had a bad merge that duplicated these theorems - once in the Ring sections (correct) and again in the Field section (redundant). The deletions are removing the redundant Field versions.

[Kim Morrison]

It's a bit confusing: usually we assume bump/v4.27.0 is in a good state. However when we get behind, I have to merge master into it manually, and sometimes this causes merge conflicts, and sometimes I resolve those incorrectly (like this time!). I don't actually bother building it, so don't notice the problem (because I will shortly be forced to notice it on nightly-testing). I then fix it on nightly-testing, and we get a confusing diff as you just discovered here. :woman_facepalming:

Not quite sure how to improve the process without making me wait around for builds...