[Merged by Bors] - chore: adaptations for nightly-2024-06-16

[kim-em]

This is mostly adaptation for leanprover/lean4#4400.

[github-actions]

PR summary 8b64a3c08f

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Set.List	211	208	-3 (-1.42%)
Mathlib.Data.List.GetD	126	125	-1 (-0.79%)
Mathlib.Data.Fintype.Basic	400	398	-2 (-0.50%)
Mathlib.Data.FinEnum	402	400	-2 (-0.50%)
Mathlib.GroupTheory.Perm.List	418	416	-2 (-0.48%)
Mathlib.SetTheory.Game.PGame	423	421	-2 (-0.47%)
Mathlib.Data.List.Cycle	435	433	-2 (-0.46%)
Mathlib.Combinatorics.Young.YoungDiagram	470	468	-2 (-0.43%)
Mathlib.Dynamics.PeriodicPts	497	495	-2 (-0.40%)
Mathlib.Data.List.Basic	261	260	-1 (-0.38%)
Mathlib.Data.List.Enum	262	261	-1 (-0.38%)
Mathlib.Data.List.Infix	262	261	-1 (-0.38%)
Mathlib.Data.List.InsertNth	262	261	-1 (-0.38%)
Mathlib.Data.List.Join	262	261	-1 (-0.38%)
Mathlib.Algebra.BigOperators.Fin	526	524	-2 (-0.38%)
Mathlib.Data.List.Zip	263	262	-1 (-0.38%)
Mathlib.Data.Nat.ChineseRemainder	547	545	-2 (-0.37%)
Mathlib.Combinatorics.Enumerative.Composition	571	569	-2 (-0.35%)
Mathlib.Data.List.Nodup	311	310	-1 (-0.32%)
Mathlib.Data.List.Rotate	314	313	-1 (-0.32%)
Mathlib.Data.List.Range	318	317	-1 (-0.31%)
Mathlib.Data.List.Perm	320	319	-1 (-0.31%)
Mathlib.Data.List.EditDistance.Estimator	321	320	-1 (-0.31%)
Mathlib.Data.List.OfFn	329	328	-1 (-0.30%)
Mathlib.Data.List.Sort	336	335	-1 (-0.30%)
Mathlib.Data.List.NodupEquivFin	338	337	-1 (-0.30%)
Mathlib.Data.List.FinRange	342	341	-1 (-0.29%)
Mathlib.Algebra.BigOperators.Group.List	356	355	-1 (-0.28%)
Mathlib.Data.Vector.Basic	377	376	-1 (-0.27%)
Mathlib.Data.Vector.Zip	378	377	-1 (-0.26%)
Mathlib.Data.List.Iterate	404	403	-1 (-0.25%)
Mathlib.Computability.TuringMachine	431	430	-1 (-0.23%)
Mathlib.Data.List.ToFinsupp	476	475	-1 (-0.21%)
Mathlib.Computability.Primrec	496	495	-1 (-0.20%)
Mathlib.Computability.Partrec	501	500	-1 (-0.20%)
Mathlib.Computability.PartrecCode	502	501	-1 (-0.20%)
Mathlib.Data.Nat.Nth	637	636	-1 (-0.16%)
Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue	644	643	-1 (-0.16%)
Mathlib.Testing.SlimCheck.Functions	686	685	-1 (-0.15%)
Mathlib.SetTheory.Game.Short	767	766	-1 (-0.13%)
Mathlib.ModelTheory.Encoding	768	767	-1 (-0.13%)
Mathlib.GroupTheory.Perm.Cycle.Concrete	810	809	-1 (-0.12%)
Mathlib.Topology.Metrizable.Uniformity	833	832	-1 (-0.12%)
Mathlib.GroupTheory.Coxeter.Inversion	883	882	-1 (-0.11%)
Mathlib.LinearAlgebra.Matrix.Transvection	933	932	-1 (-0.11%)
Mathlib.Analysis.Analytic.Composition	1236	1235	-1 (-0.08%)

---

Declarations diff

+ Fin.univ_image_getElem'
+ IsPrefix.getElem
+ Nodup.erase_getElem
+ Nodup.getElem_inj_iff
+ cons_getElem_drop_succ
+ drop_take_succ_eq_cons_getElem
+ drop_take_succ_join_eq_getElem
+ drop_take_succ_join_eq_getElem'
+ formPerm_apply_getElem
+ formPerm_apply_getElem_length
+ formPerm_apply_getElem_zero
+ formPerm_apply_lt_getElem
+ formPerm_pow_apply_getElem
+ getElem?_enum
+ getElem?_enumFrom
+ getElem?_getD_replicate_default_eq
+ getElem?_getD_singleton_default_eq
+ getElem?_indexOf
+ getElem?_iterate
+ getElem?_length
+ getElem?_ofFn
+ getElem?_pmap
+ getElem?_rotate
+ getElem?_scanl_zero
+ getElem?_zip_eq_some
+ getElem?_zip_with
+ getElem?_zip_with_eq_some
+ getElem_attach
+ getElem_cyclicPermutations
+ getElem_enum
+ getElem_enumFrom
+ getElem_eq_getElem?
+ getElem_finRange
+ getElem_indexOf
+ getElem_inits
+ getElem_insertNth_add_succ
+ getElem_insertNth_of_lt
+ getElem_insertNth_self
+ getElem_iterate
+ getElem_map_rev
+ getElem_ofFn
+ getElem_ofFn_go
+ getElem_permutations'Aux
+ getElem_pmap
+ getElem_reverse
+ getElem_reverse_aux₂
+ getElem_rotate
+ getElem_scanl_zero
+ getElem_set_of_ne
+ getElem_splitWrtComposition
+ getElem_splitWrtComposition'
+ getElem_splitWrtCompositionAux
+ getElem_tails
+ getElem_zip
+ getElem_zipWith
+ indexOf_getElem
+ neg_def
+ nodup_iff_getElem?_ne_getElem?
+ nodup_iff_injective_getElem
+ ofFn_getElem
+ ofFn_getElem_eq_map
- ext_get?
-+-+ norm_eq_ciSup

You can run this locally as follows

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

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

[dupuisf]

Thanks!

bors d+

[mathlib-bors]

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

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into bump/v4.10.0.

Build succeeded:

• Build
• Lint style