batteries#1385 adaptations for nightly-2025-08-20

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2025-08-20 batteries#1385 Please review this PR. At the end of the month this diff will land in 'main'.

[Kim Morrison]

We didn't merge the previous one (consequences of upstreaming Rat), and this one has some further import changes from changes to Lean's order typeclasses.

I'll merge this now.