chore: adaptations for nightly-2025-01-30

[kim-em]

No description provided.

[github-actions]

PR summary f21b8d948f

Import changes exceeding 2%

%	File
+4.76%	Mathlib.Lean.Meta.KAbstractPositions

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Lean.Meta.KAbstractPositions	21	22	+1 (+4.76%)
Mathlib.Tactic.MoveAdd	135	136	+1 (+0.74%)
Mathlib.Data.List.Basic	267	268	+1 (+0.37%)
Mathlib.Data.List.Indexes	268	269	+1 (+0.37%)
Mathlib.Data.List.MinMax	303	304	+1 (+0.33%)
Mathlib.Data.List.Nodup	342	343	+1 (+0.29%)
Mathlib.Data.List.FinRange	354	355	+1 (+0.28%)
Mathlib.Data.List.NodupEquivFin	370	371	+1 (+0.27%)
Mathlib.Data.FinEnum	463	464	+1 (+0.22%)
Mathlib.Data.Finset.Sort	491	492	+1 (+0.20%)
Mathlib.Logic.Equiv.List	509	510	+1 (+0.20%)
Mathlib.Computability.Primrec	570	571	+1 (+0.18%)
Mathlib.LinearAlgebra.Multilinear.Basic	878	879	+1 (+0.11%)
Mathlib.GroupTheory.Perm.Cycle.Basic	912	913	+1 (+0.11%)

Import changes for all files

Files	Import difference
There are 5670 files with changed transitive imports taking up over 235378 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ exists_mem_zipIdx
+ exists_mem_zipIdx'
+ forall_mem_zipIdx
+ forall_mem_zipIdx'
+ getElem?_idxOf
+ getElem_idxOf
+ get_idxOf
+ idxOf_append_of_mem
+ idxOf_append_of_not_mem
+ idxOf_cons_eq
+ idxOf_cons_ne
+ idxOf_eq_length_iff
+ idxOf_finRange
+ idxOf_get
+ idxOf_get?
+ idxOf_getElem
+ idxOf_inj
+ idxOf_le_length
+ idxOf_lt_length_iff
+ idxOf_of_not_mem
+ list_idxOf
+ list_idxOf₁
+ mem_ofFn'
+ nodup_zipIdx_map_snd
+ ofDigits_eq_sum_mapIdx_aux
+ toFinsupp_eq_sum_mapIdx_single
++-- up_inj
- append_eq_nil_iff
- div_le_div_left
- div_pos
- enumFrom_get?
- enum_get?
- get?_enum
- get?_enumFrom
- get_enum
- get_enumFrom
- indexOf_cons_self
- indexOf_eq_length
- indexOf_eq_length_iff
- indexOf_lt_length
- map_pmap
- mem_enum_iff_get?
- mem_ofFn
- mk_add_mem_enumFrom_iff_get?
- mk_mem_enumFrom_iff_le_and_get?_sub
- mk_mem_enum_iff_get?
- ofDigits_eq_sum_map_with_index_aux
- pmap_eq_map
- replicate_append_replicate

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.

---

Increase in tech debt: (relative, absolute) = (2.90, 0.03)

Current number	Change	Type
4267	-1	porting notes
104	3	disabled deprecation lints

Current commit f21b8d948f
Reference commit 4c900bfc52

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).