chore: adaptations for nightly-2024-09-11

[jcommelin]

No description provided.

[github-actions]

PR summary f2afc35678

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Nat.Cast.NeZero	96	76	-20 (-20.83%)
Mathlib.Algebra.CharZero.Defs	104	103	-1 (-0.96%)
Mathlib.Algebra.Order.ZeroLEOne	118	117	-1 (-0.85%)
Mathlib.Data.PNat.Defs	137	136	-1 (-0.73%)

Import changes for all files

Files	Import difference
Mathlib.Data.Nat.Cast.NeZero	-20
9 files Mathlib.Data.Nat.Cast.WithTop Mathlib.Data.PNat.Equiv Mathlib.Data.PNat.Defs Mathlib.Algebra.Order.ZeroLEOne Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Algebra.CharZero.Defs Mathlib.Algebra.Order.SuccPred Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.Algebra.Ring.Nat	-1

---

Declarations diff

+ binaryRec_one
- Nat.pos_of_neZero
- NeZero
- NeZero.ne
- NeZero.ne'
- Zero.{u}
- append_eq_cons_iff
- cons_eq_append_iff
- countP_join
- count_join
- getElem_attach
- getLast?_isSome
- instance (priority := 200) Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α
- instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0)
- map_bind
- map_pbind
- map_tail
- mem_of_mem_getLast?
- mem_of_mem_head?
- neZero_iff
- neZero_zero_iff_false
- pmap_eq_none_iff
- pmap_eq_some_iff
- pmap_none
- pmap_some
- succ
- toExpr
- xor_assoc
- xor_comm
- xor_self
- xor_zero
- zero_xor

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[TwoFX]

LGTM except for the failing build.
bors d+

[mathlib-bors]

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.