diff --git a/.github/dependabot.yml b/.github/dependabot.yml
new file mode 100644
index 000000000000..65b0787a19c9
--- /dev/null
+++ b/.github/dependabot.yml
@@ -0,0 +1,8 @@
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "monthly"
+    commit-message:
+      prefix: "chore: CI"
\ No newline at end of file
diff --git a/.github/workflows/actionlint.yml b/.github/workflows/actionlint.yml
index b539fbe3cc8f..f30abcc57578 100644
--- a/.github/workflows/actionlint.yml
+++ b/.github/workflows/actionlint.yml
@@ -17,6 +17,6 @@ jobs:
     - name: Checkout
       uses: actions/checkout@v4
     - name: actionlint
-      uses: raven-actions/actionlint@v1
+      uses: raven-actions/actionlint@v2
       with:
         pyflakes: false # we do not use python scripts
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c09f76cfbcc6..2ee6b966bac7 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -492,7 +492,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -536,7 +536,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         with:
           body_path: diff.md
           prerelease: true
diff --git a/.github/workflows/nix-ci.yml b/.github/workflows/nix-ci.yml
index 9c93570f6e8f..2ed162130637 100644
--- a/.github/workflows/nix-ci.yml
+++ b/.github/workflows/nix-ci.yml
@@ -129,7 +129,7 @@ jobs:
           python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
           echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
       - name: Publish manual to Netlify
-        uses: nwtgck/actions-netlify@v2.0
+        uses: nwtgck/actions-netlify@v3.0
         id: publish-manual
         with:
           publish-dir: ./dist
diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
index e4d6945f7058..a188dfa7b0b2 100644
--- a/.github/workflows/pr-release.yml
+++ b/.github/workflows/pr-release.yml
@@ -60,7 +60,7 @@ jobs:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
diff --git a/.github/workflows/stale.yml b/.github/workflows/stale.yml
index 42a37e5f1a26..65851b0ef851 100644
--- a/.github/workflows/stale.yml
+++ b/.github/workflows/stale.yml
@@ -11,7 +11,7 @@ jobs:
   stale:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/stale@v8
+      - uses: actions/stale@v9
         with:
           days-before-stale: -1
           days-before-pr-stale: 30
diff --git a/RELEASES.md b/RELEASES.md
index 51d2ff0c8ddf..9483bd8219b6 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -21,7 +21,315 @@ Release candidate, release notes will be copied from the branch `releases/v4.14.
 v4.13.0
 ----------
 
-Release candidate, release notes will be copied from the branch `releases/v4.13.0` once completed.
+**Full Changelog**: https://github.com/leanprover/lean4/compare/v4.12.0...v4.13.0
+
+### Language features, tactics, and metaprograms
+
+* `structure` command
+  * [#5511](https://github.com/leanprover/lean4/pull/5511) allows structure parents to be type synonyms.
+  * [#5531](https://github.com/leanprover/lean4/pull/5531) allows default values for structure fields to be noncomputable.
+
+* `rfl` and `apply_rfl` tactics
+  * [#3714](https://github.com/leanprover/lean4/pull/3714), [#3718](https://github.com/leanprover/lean4/pull/3718) improve the `rfl` tactic and give better error messages.
+  * [#3772](https://github.com/leanprover/lean4/pull/3772) makes `rfl` no longer use kernel defeq for ground terms.
+  * [#5329](https://github.com/leanprover/lean4/pull/5329) tags `Iff.refl` with `@[refl]` (@Parcly-Taxel)
+  * [#5359](https://github.com/leanprover/lean4/pull/5359) ensures that the `rfl` tactic tries `Iff.rfl` (@Parcly-Taxel)
+
+* `unfold` tactic
+  * [#4834](https://github.com/leanprover/lean4/pull/4834) let `unfold` do zeta-delta reduction of local definitions, incorporating functionality of the Mathlib `unfold_let` tactic.
+
+* `omega` tactic
+  * [#5382](https://github.com/leanprover/lean4/pull/5382) fixes spurious error in [#5315](https://github.com/leanprover/lean4/issues/5315)
+  * [#5523](https://github.com/leanprover/lean4/pull/5523) supports `Int.toNat`
+
+* `simp` tactic
+  * [#5479](https://github.com/leanprover/lean4/pull/5479) lets `simp` apply rules with higher-order patterns.
+
+* `induction` tactic
+  * [#5494](https://github.com/leanprover/lean4/pull/5494) fixes `induction`’s "pre-tactic" block to always be indented, avoiding unintended uses of it.
+
+* `ac_nf` tactic
+  * [#5524](https://github.com/leanprover/lean4/pull/5524) adds `ac_nf`, a counterpart to `ac_rfl`, for normalizing expressions with respect to associativity and commutativity. Tests it with `BitVec` expressions.
+
+* `bv_decide`
+  * [#5211](https://github.com/leanprover/lean4/pull/5211) makes `extractLsb'` the primitive `bv_decide` understands, rather than `extractLsb` (@alexkeizer)
+  * [#5365](https://github.com/leanprover/lean4/pull/5365) adds `bv_decide` diagnoses.
+  * [#5375](https://github.com/leanprover/lean4/pull/5375) adds `bv_decide` normalization rules for `ofBool (a.getLsbD i)` and `ofBool a[i]` (@alexkeizer)
+  * [#5423](https://github.com/leanprover/lean4/pull/5423) enhances the rewriting rules of `bv_decide`
+  * [#5433](https://github.com/leanprover/lean4/pull/5433) presents the `bv_decide` counterexample at the API
+  * [#5484](https://github.com/leanprover/lean4/pull/5484) handles `BitVec.ofNat` with `Nat` fvars in `bv_decide`
+  * [#5506](https://github.com/leanprover/lean4/pull/5506), [#5507](https://github.com/leanprover/lean4/pull/5507) add `bv_normalize` rules.
+  * [#5568](https://github.com/leanprover/lean4/pull/5568) generalize the `bv_normalize` pipeline to support more general preprocessing passes
+  * [#5573](https://github.com/leanprover/lean4/pull/5573) gets `bv_normalize` up-to-date with the current `BitVec` rewrites
+  * Cleanups: [#5408](https://github.com/leanprover/lean4/pull/5408), [#5493](https://github.com/leanprover/lean4/pull/5493), [#5578](https://github.com/leanprover/lean4/pull/5578)
+
+
+* Elaboration improvements
+  * [#5266](https://github.com/leanprover/lean4/pull/5266) preserve order of overapplied arguments in `elab_as_elim` procedure.
+  * [#5510](https://github.com/leanprover/lean4/pull/5510) generalizes `elab_as_elim` to allow arbitrary motive applications.
+  * [#5283](https://github.com/leanprover/lean4/pull/5283), [#5512](https://github.com/leanprover/lean4/pull/5512) refine how named arguments suppress explicit arguments. Breaking change: some previously omitted explicit arguments may need explicit `_` arguments now.
+  * [#5376](https://github.com/leanprover/lean4/pull/5376) modifies projection instance binder info for instances, making parameters that are instance implicit in the type be implicit.
+  * [#5402](https://github.com/leanprover/lean4/pull/5402) localizes universe metavariable errors to `let` bindings and `fun` binders if possible. Makes "cannot synthesize metavariable" errors take precedence over unsolved universe level errors.
+  * [#5419](https://github.com/leanprover/lean4/pull/5419) must not reduce `ite` in the discriminant of `match`-expression when reducibility setting is `.reducible`
+  * [#5474](https://github.com/leanprover/lean4/pull/5474) have autoparams report parameter/field on failure
+  * [#5530](https://github.com/leanprover/lean4/pull/5530) makes automatic instance names about types with hygienic names be hygienic.
+
+* Deriving handlers
+  * [#5432](https://github.com/leanprover/lean4/pull/5432) makes `Repr` deriving instance handle explicit type parameters
+
+* Functional induction
+  * [#5364](https://github.com/leanprover/lean4/pull/5364) adds more equalities in context, more careful cleanup.
+
+* Linters
+  * [#5335](https://github.com/leanprover/lean4/pull/5335) fixes the unused variables linter complaining about match/tactic combinations
+  * [#5337](https://github.com/leanprover/lean4/pull/5337) fixes the unused variables linter complaining about some wildcard patterns
+
+* Other fixes
+  * [#4768](https://github.com/leanprover/lean4/pull/4768) fixes a parse error when `..` appears with a `.` on the next line
+
+* Metaprogramming
+  * [#3090](https://github.com/leanprover/lean4/pull/3090) handles level parameters in `Meta.evalExpr` (@eric-wieser)  
+  * [#5401](https://github.com/leanprover/lean4/pull/5401) instance for `Inhabited (TacticM α)` (@alexkeizer)
+  * [#5412](https://github.com/leanprover/lean4/pull/5412) expose Kernel.check for debugging purposes
+  * [#5556](https://github.com/leanprover/lean4/pull/5556) improves the "invalid projection" type inference error in `inferType`.
+  * [#5587](https://github.com/leanprover/lean4/pull/5587) allows `MVarId.assertHypotheses` to set `BinderInfo` and `LocalDeclKind`.
+  * [#5588](https://github.com/leanprover/lean4/pull/5588) adds `MVarId.tryClearMany'`, a variant of `MVarId.tryClearMany`.
+
+
+
+### Language server, widgets, and IDE extensions
+
+* [#5205](https://github.com/leanprover/lean4/pull/5205) decreases the latency of auto-completion in tactic blocks.
+* [#5237](https://github.com/leanprover/lean4/pull/5237) fixes symbol occurrence highlighting in VS Code not highlighting occurrences when moving the text cursor into the identifier from the right.
+* [#5257](https://github.com/leanprover/lean4/pull/5257) fixes several instances of incorrect auto-completions being reported.
+* [#5299](https://github.com/leanprover/lean4/pull/5299) allows auto-completion to report completions for global identifiers when the elaborator fails to provide context-specific auto-completions.
+* [#5312](https://github.com/leanprover/lean4/pull/5312) fixes the server breaking when changing whitespace after the module header.
+* [#5322](https://github.com/leanprover/lean4/pull/5322) fixes several instances of auto-completion reporting non-existent namespaces.
+* [#5428](https://github.com/leanprover/lean4/pull/5428) makes sure to always report some recent file range as progress when waiting for elaboration.
+
+
+### Pretty printing
+
+* [#4979](https://github.com/leanprover/lean4/pull/4979) make pretty printer escape identifiers that are tokens.
+* [#5389](https://github.com/leanprover/lean4/pull/5389) makes formatter use the current token table.
+* [#5513](https://github.com/leanprover/lean4/pull/5513) use breakable instead of unbreakable whitespace when formatting tokens.
+
+
+### Library
+
+* [#5222](https://github.com/leanprover/lean4/pull/5222) reduces allocations in `Json.compress`.
+* [#5231](https://github.com/leanprover/lean4/pull/5231) upstreams `Zero` and `NeZero`
+* [#5292](https://github.com/leanprover/lean4/pull/5292) refactors `Lean.Elab.Deriving.FromToJson` (@arthur-adjedj)
+* [#5415](https://github.com/leanprover/lean4/pull/5415) implements `Repr Empty` (@TomasPuverle)
+* [#5421](https://github.com/leanprover/lean4/pull/5421) implements `To/FromJSON Empty` (@TomasPuverle)
+
+* Logic
+  * [#5263](https://github.com/leanprover/lean4/pull/5263) allows simplifying `dite_not`/`decide_not` with only `Decidable (¬p)`.
+  * [#5268](https://github.com/leanprover/lean4/pull/5268) fixes binders on `ite_eq_left_iff`
+  * [#5284](https://github.com/leanprover/lean4/pull/5284) turns off `Inhabited (Sum α β)` instances
+  * [#5355](https://github.com/leanprover/lean4/pull/5355) adds simp lemmas for `LawfulBEq`
+  * [#5374](https://github.com/leanprover/lean4/pull/5374) add `Nonempty` instances for products, allowing more `partial` functions to elaborate successfully
+  * [#5447](https://github.com/leanprover/lean4/pull/5447) updates Pi instance names
+  * [#5454](https://github.com/leanprover/lean4/pull/5454) makes some instance arguments implicit
+  * [#5456](https://github.com/leanprover/lean4/pull/5456) adds `heq_comm`
+  * [#5529](https://github.com/leanprover/lean4/pull/5529) moves `@[simp]` from `exists_prop'` to `exists_prop`
+
+* `Bool`
+  * [#5228](https://github.com/leanprover/lean4/pull/5228) fills gaps in Bool lemmas
+  * [#5332](https://github.com/leanprover/lean4/pull/5332) adds notation `^^` for Bool.xor
+  * [#5351](https://github.com/leanprover/lean4/pull/5351) removes `_root_.and` (and or/not/xor) and instead exports/uses `Bool.and` (etc.).
+
+* `BitVec`
+  * [#5240](https://github.com/leanprover/lean4/pull/5240) removes BitVec simps with complicated RHS
+  * [#5247](https://github.com/leanprover/lean4/pull/5247) `BitVec.getElem_zeroExtend`
+  * [#5248](https://github.com/leanprover/lean4/pull/5248) simp lemmas for BitVec, improving confluence
+  * [#5249](https://github.com/leanprover/lean4/pull/5249) removes `@[simp]` from some BitVec lemmas
+  * [#5252](https://github.com/leanprover/lean4/pull/5252) changes `BitVec.intMin/Max` from abbrev to def
+  * [#5278](https://github.com/leanprover/lean4/pull/5278) adds `BitVec.getElem_truncate` (@tobiasgrosser)
+  * [#5281](https://github.com/leanprover/lean4/pull/5281) adds udiv/umod bitblasting for `bv_decide` (@bollu)
+  * [#5297](https://github.com/leanprover/lean4/pull/5297) `BitVec` unsigned order theoretic results
+  * [#5313](https://github.com/leanprover/lean4/pull/5313) adds more basic BitVec ordering theory for UInt
+  * [#5314](https://github.com/leanprover/lean4/pull/5314) adds `toNat_sub_of_le` (@bollu)
+  * [#5357](https://github.com/leanprover/lean4/pull/5357) adds `BitVec.truncate` lemmas
+  * [#5358](https://github.com/leanprover/lean4/pull/5358) introduces `BitVec.setWidth` to unify zeroExtend and truncate (@tobiasgrosser)
+  * [#5361](https://github.com/leanprover/lean4/pull/5361) some BitVec GetElem lemmas
+  * [#5385](https://github.com/leanprover/lean4/pull/5385) adds `BitVec.ofBool_[and|or|xor]_ofBool` theorems (@tobiasgrosser)
+  * [#5404](https://github.com/leanprover/lean4/pull/5404) more of `BitVec.getElem_*` (@tobiasgrosser)
+  * [#5410](https://github.com/leanprover/lean4/pull/5410) BitVec analogues of `Nat.{mul_two, two_mul, mul_succ, succ_mul}` (@bollu)
+  * [#5411](https://github.com/leanprover/lean4/pull/5411) `BitVec.toNat_{add,sub,mul_of_lt}` for BitVector non-overflow reasoning (@bollu)
+  * [#5413](https://github.com/leanprover/lean4/pull/5413) adds `_self`, `_zero`, and `_allOnes` for `BitVec.[and|or|xor]` (@tobiasgrosser)
+  * [#5416](https://github.com/leanprover/lean4/pull/5416) adds LawCommIdentity + IdempotentOp for `BitVec.[and|or|xor]` (@tobiasgrosser)
+  * [#5418](https://github.com/leanprover/lean4/pull/5418) decidable quantifers for BitVec
+  * [#5450](https://github.com/leanprover/lean4/pull/5450) adds `BitVec.toInt_[intMin|neg|neg_of_ne_intMin]` (@tobiasgrosser)
+  * [#5459](https://github.com/leanprover/lean4/pull/5459) missing BitVec lemmas
+  * [#5469](https://github.com/leanprover/lean4/pull/5469) adds `BitVec.[not_not, allOnes_shiftLeft_or_shiftLeft, allOnes_shiftLeft_and_shiftLeft]` (@luisacicolini)
+  * [#5478](https://github.com/leanprover/lean4/pull/5478) adds `BitVec.(shiftLeft_add_distrib, shiftLeft_ushiftRight)` (@luisacicolini)
+  * [#5487](https://github.com/leanprover/lean4/pull/5487) adds `sdiv_eq`, `smod_eq` to allow `sdiv`/`smod` bitblasting (@bollu)
+  * [#5491](https://github.com/leanprover/lean4/pull/5491) adds `BitVec.toNat_[abs|sdiv|smod]` (@tobiasgrosser)
+  * [#5492](https://github.com/leanprover/lean4/pull/5492) `BitVec.(not_sshiftRight, not_sshiftRight_not, getMsb_not, msb_not)` (@luisacicolini)
+  * [#5499](https://github.com/leanprover/lean4/pull/5499) `BitVec.Lemmas` - drop non-terminal simps (@tobiasgrosser)
+  * [#5505](https://github.com/leanprover/lean4/pull/5505) unsimps `BitVec.divRec_succ'`
+  * [#5508](https://github.com/leanprover/lean4/pull/5508) adds `BitVec.getElem_[add|add_add_bool|mul|rotateLeft|rotateRight…` (@tobiasgrosser)
+  * [#5554](https://github.com/leanprover/lean4/pull/5554) adds `Bitvec.[add, sub, mul]_eq_xor` and `width_one_cases` (@luisacicolini)
+
+* `List`
+  * [#5242](https://github.com/leanprover/lean4/pull/5242) improve naming for `List.mergeSort` lemmas
+  * [#5302](https://github.com/leanprover/lean4/pull/5302) provide `mergeSort` comparator autoParam
+  * [#5373](https://github.com/leanprover/lean4/pull/5373) fix name of `List.length_mergeSort`
+  * [#5377](https://github.com/leanprover/lean4/pull/5377) upstream `map_mergeSort`
+  * [#5378](https://github.com/leanprover/lean4/pull/5378) modify signature of lemmas about `mergeSort`
+  * [#5245](https://github.com/leanprover/lean4/pull/5245) avoid importing `List.Basic` without List.Impl
+  * [#5260](https://github.com/leanprover/lean4/pull/5260) review of List API
+  * [#5264](https://github.com/leanprover/lean4/pull/5264) review of List API
+  * [#5269](https://github.com/leanprover/lean4/pull/5269) remove HashMap's duplicated Pairwise and Sublist
+  * [#5271](https://github.com/leanprover/lean4/pull/5271) remove @[simp] from `List.head_mem` and similar
+  * [#5273](https://github.com/leanprover/lean4/pull/5273) lemmas about `List.attach`
+  * [#5275](https://github.com/leanprover/lean4/pull/5275) reverse direction of `List.tail_map`
+  * [#5277](https://github.com/leanprover/lean4/pull/5277) more `List.attach` lemmas
+  * [#5285](https://github.com/leanprover/lean4/pull/5285) `List.count` lemmas
+  * [#5287](https://github.com/leanprover/lean4/pull/5287) use boolean predicates in `List.filter`
+  * [#5289](https://github.com/leanprover/lean4/pull/5289) `List.mem_ite_nil_left` and analogues
+  * [#5293](https://github.com/leanprover/lean4/pull/5293) cleanup of `List.findIdx` / `List.take` lemmas
+  * [#5294](https://github.com/leanprover/lean4/pull/5294) switch primes on `List.getElem_take`
+  * [#5300](https://github.com/leanprover/lean4/pull/5300) more `List.findIdx` theorems
+  * [#5310](https://github.com/leanprover/lean4/pull/5310) fix `List.all/any` lemmas
+  * [#5311](https://github.com/leanprover/lean4/pull/5311) fix `List.countP` lemmas
+  * [#5316](https://github.com/leanprover/lean4/pull/5316) `List.tail` lemma
+  * [#5331](https://github.com/leanprover/lean4/pull/5331) fix implicitness of `List.getElem_mem`
+  * [#5350](https://github.com/leanprover/lean4/pull/5350) `List.replicate` lemmas
+  * [#5352](https://github.com/leanprover/lean4/pull/5352) `List.attachWith` lemmas
+  * [#5353](https://github.com/leanprover/lean4/pull/5353) `List.head_mem_head?`
+  * [#5360](https://github.com/leanprover/lean4/pull/5360) lemmas about `List.tail`
+  * [#5391](https://github.com/leanprover/lean4/pull/5391) review of `List.erase` / `List.find` lemmas
+  * [#5392](https://github.com/leanprover/lean4/pull/5392) `List.fold` / `attach` lemmas
+  * [#5393](https://github.com/leanprover/lean4/pull/5393) `List.fold` relators
+  * [#5394](https://github.com/leanprover/lean4/pull/5394) lemmas about `List.maximum?`
+  * [#5403](https://github.com/leanprover/lean4/pull/5403) theorems about `List.toArray`
+  * [#5405](https://github.com/leanprover/lean4/pull/5405) reverse direction of `List.set_map`
+  * [#5448](https://github.com/leanprover/lean4/pull/5448) add lemmas about `List.IsPrefix` (@Command-Master)
+  * [#5460](https://github.com/leanprover/lean4/pull/5460) missing `List.set_replicate_self`
+  * [#5518](https://github.com/leanprover/lean4/pull/5518) rename `List.maximum?` to `max?`
+  * [#5519](https://github.com/leanprover/lean4/pull/5519) upstream `List.fold` lemmas
+  * [#5520](https://github.com/leanprover/lean4/pull/5520) restore `@[simp]` on `List.getElem_mem` etc.
+  * [#5521](https://github.com/leanprover/lean4/pull/5521) List simp fixes
+  * [#5550](https://github.com/leanprover/lean4/pull/5550) `List.unattach` and simp lemmas
+  * [#5594](https://github.com/leanprover/lean4/pull/5594) induction-friendly `List.min?_cons`
+
+* `Array`
+  * [#5246](https://github.com/leanprover/lean4/pull/5246) cleanup imports of Array.Lemmas
+  * [#5255](https://github.com/leanprover/lean4/pull/5255) split Init.Data.Array.Lemmas for better bootstrapping
+  * [#5288](https://github.com/leanprover/lean4/pull/5288) rename `Array.data` to `Array.toList`
+  * [#5303](https://github.com/leanprover/lean4/pull/5303) cleanup of `List.getElem_append` variants
+  * [#5304](https://github.com/leanprover/lean4/pull/5304) `Array.not_mem_empty`
+  * [#5400](https://github.com/leanprover/lean4/pull/5400) reorganization in Array/Basic
+  * [#5420](https://github.com/leanprover/lean4/pull/5420) make `Array` functions either semireducible or use structural recursion
+  * [#5422](https://github.com/leanprover/lean4/pull/5422) refactor `DecidableEq (Array α)`
+  * [#5452](https://github.com/leanprover/lean4/pull/5452) refactor of Array
+  * [#5458](https://github.com/leanprover/lean4/pull/5458) cleanup of Array docstrings after refactor
+  * [#5461](https://github.com/leanprover/lean4/pull/5461) restore `@[simp]` on `Array.swapAt!_def`
+  * [#5465](https://github.com/leanprover/lean4/pull/5465) improve Array GetElem lemmas
+  * [#5466](https://github.com/leanprover/lean4/pull/5466) `Array.foldX` lemmas
+  * [#5472](https://github.com/leanprover/lean4/pull/5472) @[simp] lemmas about `List.toArray`
+  * [#5485](https://github.com/leanprover/lean4/pull/5485) reverse simp direction for `toArray_concat`
+  * [#5514](https://github.com/leanprover/lean4/pull/5514) `Array.eraseReps`
+  * [#5515](https://github.com/leanprover/lean4/pull/5515) upstream `Array.qsortOrd`
+  * [#5516](https://github.com/leanprover/lean4/pull/5516) upstream `Subarray.empty`
+  * [#5526](https://github.com/leanprover/lean4/pull/5526) fix name of `Array.length_toList`
+  * [#5527](https://github.com/leanprover/lean4/pull/5527) reduce use of deprecated lemmas in Array
+  * [#5534](https://github.com/leanprover/lean4/pull/5534) cleanup of Array GetElem lemmas
+  * [#5536](https://github.com/leanprover/lean4/pull/5536) fix `Array.modify` lemmas
+  * [#5551](https://github.com/leanprover/lean4/pull/5551) upstream `Array.flatten` lemmas
+  * [#5552](https://github.com/leanprover/lean4/pull/5552) switch obvious cases of array "bang"`[]!` indexing to rely on hypothesis (@TomasPuverle)
+  * [#5577](https://github.com/leanprover/lean4/pull/5577) add missing simp to `Array.size_feraseIdx`
+  * [#5586](https://github.com/leanprover/lean4/pull/5586) `Array/Option.unattach`
+
+* `Option`
+  * [#5272](https://github.com/leanprover/lean4/pull/5272) remove @[simp] from `Option.pmap/pbind` and add simp lemmas
+  * [#5307](https://github.com/leanprover/lean4/pull/5307) restoring Option simp confluence
+  * [#5354](https://github.com/leanprover/lean4/pull/5354) remove @[simp] from `Option.bind_map`
+  * [#5532](https://github.com/leanprover/lean4/pull/5532) `Option.attach`
+  * [#5539](https://github.com/leanprover/lean4/pull/5539) fix explicitness of `Option.mem_toList`
+
+* `Nat`
+  * [#5241](https://github.com/leanprover/lean4/pull/5241) add @[simp] to `Nat.add_eq_zero_iff`
+  * [#5261](https://github.com/leanprover/lean4/pull/5261) Nat bitwise lemmas
+  * [#5262](https://github.com/leanprover/lean4/pull/5262) `Nat.testBit_add_one` should not be a global simp lemma
+  * [#5267](https://github.com/leanprover/lean4/pull/5267) protect some Nat bitwise theorems
+  * [#5305](https://github.com/leanprover/lean4/pull/5305) rename Nat bitwise lemmas
+  * [#5306](https://github.com/leanprover/lean4/pull/5306) add `Nat.self_sub_mod` lemma
+  * [#5503](https://github.com/leanprover/lean4/pull/5503) restore @[simp] to upstreamed `Nat.lt_off_iff`
+
+* `Int`
+  * [#5301](https://github.com/leanprover/lean4/pull/5301) rename `Int.div/mod` to `Int.tdiv/tmod`
+  * [#5320](https://github.com/leanprover/lean4/pull/5320) add `ediv_nonneg_of_nonpos_of_nonpos` to DivModLemmas (@sakehl)
+
+* `Fin`
+  * [#5250](https://github.com/leanprover/lean4/pull/5250) missing lemma about `Fin.ofNat'`
+  * [#5356](https://github.com/leanprover/lean4/pull/5356) `Fin.ofNat'` uses `NeZero`
+  * [#5379](https://github.com/leanprover/lean4/pull/5379) remove some @[simp]s from Fin lemmas
+  * [#5380](https://github.com/leanprover/lean4/pull/5380) missing Fin @[simp] lemmas
+
+* `HashMap`
+  * [#5244](https://github.com/leanprover/lean4/pull/5244) (`DHashMap`|`HashMap`|`HashSet`).(`getKey?`|`getKey`|`getKey!`|`getKeyD`)
+  * [#5362](https://github.com/leanprover/lean4/pull/5362) remove the last use of `Lean.(HashSet|HashMap)`
+  * [#5369](https://github.com/leanprover/lean4/pull/5369) `HashSet.ofArray`
+  * [#5370](https://github.com/leanprover/lean4/pull/5370) `HashSet.partition`
+  * [#5581](https://github.com/leanprover/lean4/pull/5581) `Singleton`/`Insert`/`Union` instances for `HashMap`/`Set`
+  * [#5582](https://github.com/leanprover/lean4/pull/5582) `HashSet.all`/`any`
+  * [#5590](https://github.com/leanprover/lean4/pull/5590) adding `Insert`/`Singleton`/`Union` instances for `HashMap`/`Set.Raw`
+  * [#5591](https://github.com/leanprover/lean4/pull/5591) `HashSet.Raw.all/any`
+
+* `Monads`
+  * [#5463](https://github.com/leanprover/lean4/pull/5463) upstream some monad lemmas
+  * [#5464](https://github.com/leanprover/lean4/pull/5464) adjust simp attributes on monad lemmas
+  * [#5522](https://github.com/leanprover/lean4/pull/5522) more monadic simp lemmas
+
+* Simp lemma cleanup
+  * [#5251](https://github.com/leanprover/lean4/pull/5251) remove redundant simp annotations
+  * [#5253](https://github.com/leanprover/lean4/pull/5253) remove Int simp lemmas that can't fire
+  * [#5254](https://github.com/leanprover/lean4/pull/5254) variables appearing on both sides of an iff should be implicit
+  * [#5381](https://github.com/leanprover/lean4/pull/5381) cleaning up redundant simp lemmas
+
+
+### Compiler, runtime, and FFI
+
+* [#4685](https://github.com/leanprover/lean4/pull/4685) fixes a typo in the C `run_new_frontend` signature
+* [#4729](https://github.com/leanprover/lean4/pull/4729) has IR checker suggest using `noncomputable`
+* [#5143](https://github.com/leanprover/lean4/pull/5143) adds a shared library for Lake
+* [#5437](https://github.com/leanprover/lean4/pull/5437) removes (syntactically) duplicate imports (@euprunin)
+* [#5462](https://github.com/leanprover/lean4/pull/5462) updates `src/lake/lakefile.toml` to the adjusted Lake build process
+* [#5541](https://github.com/leanprover/lean4/pull/5541) removes new shared libs before build to better support Windows
+* [#5558](https://github.com/leanprover/lean4/pull/5558) make `lean.h` compile with MSVC (@kant2002)
+* [#5564](https://github.com/leanprover/lean4/pull/5564) removes non-conforming size-0 arrays (@eric-wieser)
+
+
+### Lake
+  * Reservoir build cache. Lake will now attempt to fetch a pre-built copy of the package from Reservoir before building it. This is only enabled for packages in the leanprover or leanprover-community organizations on versions indexed by Reservoir. Users can force Lake to build packages from the source by passing --no-cache on the CLI or by setting the  LAKE_NO_CACHE environment variable to true. [#5486](https://github.com/leanprover/lean4/pull/5486), [#5572](https://github.com/leanprover/lean4/pull/5572), [#5583](https://github.com/leanprover/lean4/pull/5583), [#5600](https://github.com/leanprover/lean4/pull/5600), [#5641](https://github.com/leanprover/lean4/pull/5641), [#5642](https://github.com/leanprover/lean4/pull/5642).
+  * [#5504](https://github.com/leanprover/lean4/pull/5504) lake new and lake init now produce TOML configurations by default.
+  * [#5878](https://github.com/leanprover/lean4/pull/5878) fixes a serious issue where Lake would delete path dependencies when attempting to cleanup a dependency required with an incorrect name.
+
+  * **Breaking changes**
+    * [#5641](https://github.com/leanprover/lean4/pull/5641) A Lake build of target within a package will no longer build a package's dependencies package-level extra target dependencies. At the technical level, a package's extraDep facet no longer transitively builds its dependencies’ extraDep facets (which include their extraDepTargets).
+
+### Documentation fixes
+
+* [#3918](https://github.com/leanprover/lean4/pull/3918) `@[builtin_doc]` attribute (@digama0)
+* [#4305](https://github.com/leanprover/lean4/pull/4305) explains the borrow syntax (@eric-wieser)
+* [#5349](https://github.com/leanprover/lean4/pull/5349) adds documentation for `groupBy.loop` (@vihdzp)
+* [#5473](https://github.com/leanprover/lean4/pull/5473) fixes typo in `BitVec.mul` docstring (@llllvvuu)
+* [#5476](https://github.com/leanprover/lean4/pull/5476) fixes typos in `Lean.MetavarContext`
+* [#5481](https://github.com/leanprover/lean4/pull/5481) removes mention of `Lean.withSeconds` (@alexkeizer)
+* [#5497](https://github.com/leanprover/lean4/pull/5497) updates documentation and tests for `toUIntX` functions (@TomasPuverle)
+* [#5087](https://github.com/leanprover/lean4/pull/5087) mentions that `inferType` does not ensure type correctness
+* Many fixes to spelling across the doc-strings, (@euprunin): [#5425](https://github.com/leanprover/lean4/pull/5425) [#5426](https://github.com/leanprover/lean4/pull/5426) [#5427](https://github.com/leanprover/lean4/pull/5427) [#5430](https://github.com/leanprover/lean4/pull/5430)  [#5431](https://github.com/leanprover/lean4/pull/5431) [#5434](https://github.com/leanprover/lean4/pull/5434) [#5435](https://github.com/leanprover/lean4/pull/5435) [#5436](https://github.com/leanprover/lean4/pull/5436) [#5438](https://github.com/leanprover/lean4/pull/5438) [#5439](https://github.com/leanprover/lean4/pull/5439) [#5440](https://github.com/leanprover/lean4/pull/5440) [#5599](https://github.com/leanprover/lean4/pull/5599)
+
+### Changes to CI
+
+* [#5343](https://github.com/leanprover/lean4/pull/5343) allows addition of `release-ci` label via comment (@thorimur)
+* [#5344](https://github.com/leanprover/lean4/pull/5344) sets check level correctly during workflow (@thorimur)
+* [#5444](https://github.com/leanprover/lean4/pull/5444) Mathlib's `lean-pr-testing-NNNN` branches should use Batteries' `lean-pr-testing-NNNN` branches
+* [#5489](https://github.com/leanprover/lean4/pull/5489) commit `lake-manifest.json` when updating `lean-pr-testing` branches
+* [#5490](https://github.com/leanprover/lean4/pull/5490) use separate secrets for commenting and branching in `pr-release.yml`
 
 v4.12.0
 ----------
diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean
index f7ad5d6f1c3a..bba5c37d74e7 100644
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -23,7 +23,7 @@ theorem foldlM_eq_foldlM_toList.aux [Monad m]
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
     simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
-    rw (occs := .pos [2]) [← List.get_drop_eq_drop _ _ ‹_›]
+    rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
diff --git a/src/Init/Data/Array/GetLit.lean b/src/Init/Data/Array/GetLit.lean
index 73594b793788..f5139dc5b4d9 100644
--- a/src/Init/Data/Array/GetLit.lean
+++ b/src/Init/Data/Array/GetLit.lean
@@ -41,6 +41,6 @@ where
   getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
     rfl
   go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
-    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.get_drop_eq_drop, *]
+    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.getElem_cons_drop_succ_eq_drop, *]
 
 end Array
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index f43e625e08bb..0bf6b97dcfb5 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -10,6 +10,7 @@ import Init.Data.List.Monadic
 import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
+import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
 import Init.Data.List.OfFn
 import Init.Data.Array.Mem
@@ -246,7 +247,7 @@ where
   aux (i r) :
       mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
     unfold mapM.map; split
-    · rw [← List.get_drop_eq_drop _ i ‹_›]
+    · rw [← List.getElem_cons_drop_succ_eq_drop ‹_›]
       simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
         pure_bind]
       rfl
@@ -1460,6 +1461,10 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
+theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
+    a.feraseIdx i = a.eraseIdx i.1 := by
+  simp [eraseIdx]
+
 end Array
 
 open Array
@@ -1611,7 +1616,7 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   apply ext'
   simp
 
-@[simp] theorem toArray_extract (l : List α) (start stop : Nat) :
+@[simp] theorem extract_toArray (l : List α) (start stop : Nat) :
     l.toArray.extract start stop = ((l.drop start).take (stop - start)).toArray := by
   apply ext'
   simp
@@ -1619,6 +1624,64 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
 @[simp] theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f := by
   ext <;> simp
 
+theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
+    takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
+  rw [takeWhile.go, takeWhile.go]
+  simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+    getElem_toArray, getElem_cons_succ]
+  split
+  rw [takeWhile_go_succ]
+  rfl
+
+theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
+    Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
+  induction l generalizing i r with
+  | nil => simp [takeWhile.go]
+  | cons a l ih =>
+    rw [takeWhile.go]
+    cases i with
+    | zero =>
+      simp [takeWhile_go_succ, ih, takeWhile_cons]
+      split <;> simp
+    | succ i =>
+      simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+        getElem_toArray, getElem_cons_succ, drop_succ_cons]
+      split <;> rename_i h₁
+      · rw [takeWhile_go_succ, ih]
+        rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
+        split <;> simp_all
+      · simp_all [drop_eq_nil_of_le]
+
+@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
+    l.toArray.takeWhile p = (l.takeWhile p).toArray := by
+  simp [Array.takeWhile, takeWhile_go_toArray]
+
+@[simp] theorem feraseIdx_toArray (l : List α) (i : Fin l.toArray.size) :
+    l.toArray.feraseIdx i = (l.eraseIdx i).toArray := by
+  rw [feraseIdx]
+  split <;> rename_i h
+  · rw [feraseIdx_toArray]
+    simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
+    rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
+    simp
+  · rcases i with ⟨i, w⟩
+    simp at h w
+    have t : i = l.length - 1 := by omega
+    simp [t]
+termination_by l.length - i
+decreasing_by
+  rename_i h
+  simp at h
+  simp
+  omega
+
+@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) :
+    l.toArray.eraseIdx i = (l.eraseIdx i).toArray := by
+  rw [Array.eraseIdx]
+  split
+  · simp
+  · simp_all [eraseIdx_eq_self.2]
+
 end List
 
 namespace Array
@@ -1629,6 +1692,20 @@ namespace Array
 @[simp] theorem toList_ofFn (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f := by
   apply List.ext_getElem <;> simp
 
+@[simp] theorem toList_takeWhile (p : α → Bool) (as : Array α) :
+    (as.takeWhile p).toList = as.toList.takeWhile p := by
+  induction as; simp
+
+@[simp] theorem toList_feraseIdx (as : Array α) (i : Fin as.size) :
+    (as.feraseIdx i).toList = as.toList.eraseIdx i.1 := by
+  induction as
+  simp
+
+@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) :
+    (as.eraseIdx i).toList = as.toList.eraseIdx i := by
+  induction as
+  simp
+
 end Array
 
 /-! ### Deprecations -/
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index 925ccdf55ee5..f0a07e025f4d 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -169,6 +169,13 @@ theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Li
     (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by
   simp
 
+theorem pmap_eq_self {l : List α} {p : α → Prop} (hp : ∀ (a : α), a ∈ l → p a)
+    (f : (a : α) → p a → α) : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by
+  rw [pmap_eq_map_attach]
+  conv => lhs; rhs; rw [← attach_map_subtype_val l]
+  rw [map_inj_left]
+  simp
+
 @[simp]
 theorem attach_eq_nil_iff {l : List α} : l.attach = [] ↔ l = [] :=
   pmap_eq_nil_iff
diff --git a/src/Init/Data/List/Nat/Erase.lean b/src/Init/Data/List/Nat/Erase.lean
index 5c1e4adfabd8..e17996016580 100644
--- a/src/Init/Data/List/Nat/Erase.lean
+++ b/src/Init/Data/List/Nat/Erase.lean
@@ -64,3 +64,82 @@ theorem getElem_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : j < (l.era
     (l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
   rw [getElem_eraseIdx, dif_neg]
   omega
+
+theorem eraseIdx_set_eq {l : List α} {i : Nat} {a : α} :
+    (l.set i a).eraseIdx i = l.eraseIdx i := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    rw [getElem_eraseIdx, getElem_eraseIdx]
+    split <;>
+    · rw [getElem_set_ne]
+      omega
+
+theorem eraseIdx_set_lt {l : List α} {i : Nat} {j : Nat} {a : α} (h : j < i) :
+    (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    simp only [length_eraseIdx, length_set] at h₁
+    simp only [getElem_eraseIdx, getElem_set]
+    split
+    · split
+      · split
+        · rfl
+        · omega
+      · split
+        · omega
+        · rfl
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : i - 1 ≠ n := by omega
+        simp [t]
+
+theorem eraseIdx_set_gt {l : List α} {i : Nat} {j : Nat} {a : α} (h : i < j) :
+    (l.set i a).eraseIdx j = (l.eraseIdx j).set i a := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    simp only [length_eraseIdx, length_set] at h₁
+    simp only [getElem_eraseIdx, getElem_set]
+    split
+    · rfl
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : i ≠ n := by omega
+        simp [t]
+
+@[simp] theorem set_getElem_succ_eraseIdx_succ
+    {l : List α} {i : Nat} (h : i + 1 < l.length) :
+    (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i := by
+  apply ext_getElem
+  · simp only [length_set, length_eraseIdx, h, ↓reduceIte]
+    rw [if_pos]
+    omega
+  · intro n h₁ h₂
+    simp [getElem_set, getElem_eraseIdx]
+    split
+    · split
+      · omega
+      · simp_all
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : ¬ n < i := by omega
+        simp [t]
+
+@[simp] theorem eraseIdx_length_sub_one (l : List α) :
+    (l.eraseIdx (l.length - 1)) = l.dropLast := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+    omega
+  · intro n h₁ h₂
+    rw [getElem_eraseIdx_of_lt, getElem_dropLast]
+    simp_all
+
+end List
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index 771341a13339..c3ec7f34137d 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -190,7 +190,7 @@ theorem set_drop {l : List α} {n m : Nat} {a : α} :
 theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
     (l.take i).concat l[i] = l.take (i+1) :=
   Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by
-    rw [concat_eq_append, append_assoc, singleton_append, get_drop_eq_drop, take_append_drop]
+    rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop_succ_eq_drop, take_append_drop]
 
 @[deprecated take_succ_cons (since := "2024-07-25")]
 theorem take_cons_succ : (a::as).take (i+1) = a :: as.take i := rfl
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 786bb371c7c8..d7f07a3db65f 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -374,9 +374,15 @@ end choice
 
 -- See `Init.Data.Option.List` for lemmas about `toList`.
 
-@[simp] theorem or_some : (some a).or o = some a := rfl
+@[simp] theorem some_or : (some a).or o = some a := rfl
 @[simp] theorem none_or : none.or o = o := rfl
 
+@[deprecated some_or (since := "2024-11-03")] theorem or_some : (some a).or o = some a := rfl
+
+/-- This will be renamed to `or_some` once the existing deprecated lemma is removed. -/
+@[simp] theorem or_some' {o : Option α} : o.or (some a) = o.getD a := by
+  cases o <;> rfl
+
 theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
   cases o <;> rfl
 
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index 2906fd3204ea..22119ef6c162 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -211,10 +211,13 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where
   | _ :: _, 0, _ => .head ..
   | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
 
-theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
+theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.length) :
+    as[i] :: as.drop (i+1) = as.drop i :=
   match as, i with
   | _::_, 0   => rfl
-  | _::_, i+1 => get_drop_eq_drop _ i _
+  | _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) _
+
+@[deprecated (since := "2024-11-05")] abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop
 
 end List