Merge main into nightly-testing

Author: leanprover-community-mathlib4-bot

README.md

@@ -75,12 +75,13 @@ Batteries PRs often affect Mathlib, a key component of the Lean ecosystem.
 When Batteries changes in a significant way, Mathlib must adapt promptly.
 When necessary, Batteries contributors are expected to either create an adaptation PR on Mathlib, or ask for assistance for and to collaborate with this necessary process.
 
-Every Batteries PR has an automatically created Mathlib branch called `batteries-pr-testing-N` where `N` is the number of the Batteries PR.
+Every Batteries PR has an automatically created [Mathlib Nightly Testing](https://github.com/leanprover-community/mathlib4-nightly-testing/) branch called `batteries-pr-testing-N` where `N` is the number of the Batteries PR.
 This is a clone of Mathlib where the Batteries requirement points to the Batteries PR branch instead of the main branch.
 Batteries uses this branch to check whether the Batteries PR needs Mathlib adaptations.
 A tag `builds-mathlib` will be issued when this branch needs no adaptation; a tag `breaks-mathlib` will be issued when the branch does need an adaptation.
 
 The first step in creating an adaptation PR is to switch to the `batteries-pr-testing-N` branch and push changes to that branch until the Mathlib CI process works.
+You may need to ask for write access to [Mathlib Nightly Testing](https://github.com/leanprover-community/mathlib4-nightly-testing/) to do that.
 Changes to the Batteries PR will be integrated automatically as you work on this process.
 Do not redirect the Batteries requirement to main until the Batteries PR is merged.
 Please ask questions to Batteries and Mathlib maintainers if you run into issues with this process.