nightly#61 adaptations for nightly-2025-09-12

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2025-09-12 nightly#61 Please review this PR. At the next toolchain release this diff will land in 'master'.

[Kevin Buzzard]

This looks fine other than the changes to Mathlib/Tactic/ which I am not competent to review. One observation is that the code added in Tactic/CategoryTheory/Reassocl.lean is stuff which was moved from Tactic/CategoryTheory/Refs.lean as this file was deleted. But most of the other stuff is beyond me.

[Robin Arnez]

Kevin Buzzard schrieb:

One observation is that the code added in Tactic/CategoryTheory/Reassoc.lean is stuff which was moved from Tactic/CategoryTheory/Refs.lean as this file was deleted.

Yeah, this reverts a previous adaptation and puts it back in sync with mathlib master

[Kevin Buzzard]

I'm just saying that if someone wants to review the meta code then they don't need to get confused by that part :-) but I was confused by all the other parts.

[Robin Arnez]

Most of the other stuff is related to Verso doc-strings I believe, so it'd probably best if @David Thrane Christiansen looked over this

[Kim Morrison]

'd