chore: adaptations for nightly-2025-06-17 (#26043)

leanprover-community-mathlib4-bot · JovanGerb · jcommelin · web-flow · commit 6f9fba5fa8ad · 2025-06-17T18:53:02.000+02:00
* revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 --------- Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de>
diff --git a/Mathlib/Algebra/BigOperators/Group/List/Basic.lean b/Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@@ -487,15 +487,15 @@ lemma take_sum_flatten (L : List (List α)) (i : ℕ) :
     L.flatten.take ((L.map length).take i).sum = (L.take i).flatten := by
   induction L generalizing i
   · simp
-  · cases i <;> simp [take_append, *]
+  · cases i <;> simp [take_length_add_append, *]
 
 /-- In a flatten, dropping all the elements up to an index which is the sum of the lengths of the
 first `i` sublists, is the same as taking the join after dropping the first `i` sublists. -/
 lemma drop_sum_flatten (L : List (List α)) (i : ℕ) :
     L.flatten.drop ((L.map length).take i).sum = (L.drop i).flatten := by
   induction L generalizing i
   · simp
-  · cases i <;> simp [take_append, *]
+  · cases i <;> simp [take_length_add_append, *]
 
 @[deprecated (since := "2024-10-25")] alias take_sum_join' := take_sum_flatten
 @[deprecated (since := "2024-10-25")] alias drop_sum_join' := drop_sum_flatten
diff --git a/Mathlib/Combinatorics/Enumerative/DyckWord.lean b/Mathlib/Combinatorics/Enumerative/DyckWord.lean
@@ -71,7 +71,7 @@ instance : Coe DyckWord (List DyckStep) := ⟨DyckWord.toList⟩
 instance : Add DyckWord where
   add p q := ⟨p ++ q, by
     simp only [count_append, p.count_U_eq_count_D, q.count_U_eq_count_D], by
-    simp only [take_append_eq_append_take, count_append]
+    simp only [take_append, count_append]
     exact fun _ ↦ add_le_add (p.count_D_le_count_U _) (q.count_D_le_count_U _)⟩
 
 instance : Zero DyckWord := ⟨[], by simp, by simp⟩
@@ -160,7 +160,7 @@ def nest : DyckWord where
   toList := [U] ++ p ++ [D]
   count_U_eq_count_D := by simp [p.count_U_eq_count_D]
   count_D_le_count_U i := by
-    simp only [take_append_eq_append_take, count_append]
+    simp only [take_append, count_append]
     rw [← add_rotate (count D _), ← add_rotate (count U _)]
     apply add_le_add _ (p.count_D_le_count_U _)
     rcases i.eq_zero_or_pos with hi | hi; · simp [hi]
@@ -180,7 +180,7 @@ def IsNested : Prop :=
 protected lemma IsNested.nest : p.nest.IsNested := ⟨nest_ne_zero, fun i lb ub ↦ by
   simp_rw [nest, length_append, length_singleton] at ub ⊢
   rw [take_append_of_le_length (by rw [singleton_append, length_cons]; omega),
-    take_append_eq_append_take, take_of_length_le (by rw [length_singleton]; omega),
+    take_append, take_of_length_le (by rw [length_singleton]; omega),
     length_singleton, singleton_append, count_cons_of_ne (by simp), count_cons_self,
     Nat.lt_add_one_iff]
   exact p.count_D_le_count_U _⟩
@@ -293,10 +293,10 @@ lemma firstReturn_add : (p + q).firstReturn = if p = 0 then q.firstReturn else p
   · simp_rw [u, decide_eq_true_eq, getElem_range]
     have v := firstReturn_lt_length h
     constructor
-    · rw [take_append_eq_append_take, show p.firstReturn + 1 - p.toList.length = 0 by omega,
+    · rw [take_append, show p.firstReturn + 1 - p.toList.length = 0 by omega,
         take_zero, append_nil, count_take_firstReturn_add_one h]
     · intro j hj
-      rw [take_append_eq_append_take, show j + 1 - p.toList.length = 0 by omega,
+      rw [take_append, show j + 1 - p.toList.length = 0 by omega,
         take_zero, append_nil]
       simpa using (count_D_lt_count_U_of_lt_firstReturn hj).ne'
   · rw [length_range, u, length_append]
@@ -311,7 +311,7 @@ lemma firstReturn_nest : p.nest.firstReturn = p.toList.length + 1 := by
     · rw [take_of_length_le (by simp), ← u, p.nest.count_U_eq_count_D]
     · intro j hj
       simp_rw [cons_append, take_succ_cons, count_cons, beq_self_eq_true, ite_true,
-        beq_iff_eq, reduceCtorEq, ite_false, take_append_eq_append_take,
+        beq_iff_eq, reduceCtorEq, ite_false, take_append,
         show j - p.toList.length = 0 by omega, take_zero, append_nil]
       have := p.count_D_le_count_U j
       simp only [add_zero, decide_eq_false_iff_not, ne_eq]
diff --git a/Mathlib/Data/List/DropRight.lean b/Mathlib/Data/List/DropRight.lean
@@ -53,8 +53,8 @@ theorem rdrop_eq_reverse_drop_reverse : l.rdrop n = reverse (l.reverse.drop n) :
   induction' l using List.reverseRecOn with xs x IH generalizing n
   · simp
   · cases n
-    · simp [take_append]
-    · simp [take_append_eq_append_take, IH]
+    · simp [take_length_add_append]
+    · simp [take_append, IH]
 
 @[simp]
 theorem rdrop_concat_succ (x : α) : rdrop (l ++ [x]) (n + 1) = rdrop l n := by
@@ -76,7 +76,7 @@ theorem rtake_eq_reverse_take_reverse : l.rtake n = reverse (l.reverse.take n) :
   · simp
   · cases n
     · exact drop_length
-    · simp [drop_append_eq_append_drop, IH]
+    · simp [drop_append, IH]
 
 @[simp]
 theorem rtake_concat_succ (x : α) : rtake (l ++ [x]) (n + 1) = rtake l n ++ [x] := by
diff --git a/Mathlib/Data/List/InsertIdx.lean b/Mathlib/Data/List/InsertIdx.lean
@@ -29,7 +29,7 @@ variable {a : α}
 
 @[simp]
 theorem sublist_insertIdx (l : List α) (n : ℕ) (a : α) : l <+ (l.insertIdx n a) := by
-  simpa only [eraseIdx_insertIdx] using eraseIdx_sublist (l.insertIdx n a) n
+  simpa only [eraseIdx_insertIdx_self] using eraseIdx_sublist (l.insertIdx n a) n
 
 @[simp]
 theorem subset_insertIdx (l : List α) (n : ℕ) (a : α) : l ⊆ l.insertIdx n a :=
@@ -40,7 +40,7 @@ is the same as setting `n`th element to `a`.
 
 We assume that `n ≠ length l`, because otherwise LHS equals `l ++ [a]` while RHS equals `l`. -/
 @[simp]
-theorem insertIdx_eraseIdx {l : List α} {n : ℕ} (hn : n ≠ length l) (a : α) :
+theorem insertIdx_eraseIdx_self {l : List α} {n : ℕ} (hn : n ≠ length l) (a : α) :
     (l.eraseIdx n).insertIdx n a = l.set n a := by
   induction n generalizing l <;> cases l <;> simp_all
 
diff --git a/Mathlib/Data/List/Perm/Basic.lean b/Mathlib/Data/List/Perm/Basic.lean
@@ -44,7 +44,7 @@ theorem Perm.subset_congr_right {l₁ l₂ l₃ : List α} (h : l₁ ~ l₂) : l
 
 theorem set_perm_cons_eraseIdx {n : ℕ} (h : n < l.length) (a : α) :
     l.set n a ~ a :: l.eraseIdx n := by
-  rw [← insertIdx_eraseIdx h.ne]
+  rw [← insertIdx_eraseIdx_self h.ne]
   apply perm_insertIdx
   rw [length_eraseIdx_of_lt h]
   exact Nat.le_sub_one_of_lt h
diff --git a/Mathlib/Data/List/TakeDrop.lean b/Mathlib/Data/List/TakeDrop.lean
@@ -44,7 +44,7 @@ theorem take_one_drop_eq_of_lt_length {l : List α} {n : ℕ} (h : n < l.length)
 
 @[simp] lemma take_eq_left_iff {x y : List α} {n : ℕ} :
     (x ++ y).take n = x.take n ↔ y = [] ∨ n ≤ x.length := by
-  simp [take_append_eq_append_take, Nat.sub_eq_zero_iff_le, Or.comm]
+  simp [take_append, Nat.sub_eq_zero_iff_le, Or.comm]
 
 @[simp] lemma left_eq_take_iff {x y : List α} {n : ℕ} :
     x.take n = (x ++ y).take n ↔ y = [] ∨ n ≤ x.length := by
diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean
@@ -534,9 +534,12 @@ theorem insertIdx_val {i : Fin (n + 1)} {v : Vector α n} :
 theorem eraseIdx_val {i : Fin n} : ∀ {v : Vector α n}, (eraseIdx i v).val = v.val.eraseIdx i
   | _ => rfl
 
-theorem eraseIdx_insertIdx {v : Vector α n} {i : Fin (n + 1)} :
+theorem eraseIdx_insertIdx_self {v : Vector α n} {i : Fin (n + 1)} :
     eraseIdx i (insertIdx a i v) = v :=
-  Subtype.eq (List.eraseIdx_insertIdx ..)
+  Subtype.eq (List.eraseIdx_insertIdx_self ..)
+
+@[deprecated (since := "2025-06-17")]
+alias eraseIdx_insertIdx := eraseIdx_insertIdx_self
 
 /-- Erasing an element after inserting an element, at different indices. -/
 theorem eraseIdx_insertIdx' {v : Vector α (n + 1)} :
diff --git a/Mathlib/GroupTheory/Coxeter/Inversion.lean b/Mathlib/GroupTheory/Coxeter/Inversion.lean
@@ -421,8 +421,8 @@ theorem IsReduced.nodup_rightInvSeq {ω : List B} (rω : cs.IsReduced ω) : List
   have h₃ : t' = (ris ω).getD j' 1                    := by
     rw [h₂, cs.getD_rightInvSeq, cs.getD_rightInvSeq,
       (Nat.sub_add_cancel (by omega) : j' - 1 + 1 = j'), eraseIdx_eq_take_drop_succ,
-      drop_append_eq_append_drop, drop_of_length_le (by simp [j_lt_j'.le]), length_take,
-      drop_drop, nil_append, min_eq_left_of_lt (j_lt_j'.trans j'_lt_length), Nat.add_comm,
+      drop_append, drop_of_length_le (by simp [j_lt_j'.le]), length_take, drop_drop,
+      nil_append, min_eq_left_of_lt (j_lt_j'.trans j'_lt_length), Nat.add_comm,
       ← add_assoc, Nat.sub_add_cancel (by omega), mul_left_inj, mul_right_inj]
     congr 2
     show (List.take j ω ++ List.drop (j + 1) ω)[j' - 1]? = ω[j']?
diff --git a/Mathlib/ModelTheory/Encoding.lean b/Mathlib/ModelTheory/Encoding.lean
@@ -256,8 +256,8 @@ theorem listDecode_encode_list (l : List (Σ n, L.BoundedFormula α n)) :
     · obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
       rw [cast_eq_iff_heq]
       exact (Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2
-    rw [List.drop_append_eq_append_drop, length_map, length_finRange, Nat.sub_self, drop,
-      drop_eq_nil_of_le, nil_append]
+    rw [List.drop_append, length_map, length_finRange, Nat.sub_self, drop, drop_eq_nil_of_le,
+      nil_append]
     rw [length_map, length_finRange]
   | imp _ _ ih1 ih2 =>
     intro l
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "535804a65d81e5dee7319be86c548ac649e8c047",
+   "rev": "481cbb4065fba7ba938c217c41f1a28b55207e2f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-16
+leanprover/lean4:nightly-2025-06-17
