chore: adaptations for nightly-2025-06-16 (#25994)

* chore: bump to nightly-2025-06-03

* fix

* fix

* Update lean-toolchain for testing leanprover/lean4#8610

* fix

* 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 <[email protected]>

* 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

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Jovan Gerbscheid <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>
Co-authored-by: sgouezel <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>

Author: 11 people

Mathlib/Combinatorics/SimpleGraph/Path.lean

@@ -271,7 +271,7 @@ lemma isCycle_reverse {p : G.Walk u u} : p.reverse.IsCycle ↔ p.IsCycle where
 lemma IsCycle.isPath_of_append_right {p : G.Walk u v} {q : G.Walk v u} (h : ¬ p.Nil)
     (hcyc : (p.append q).IsCycle) : q.IsPath := by
   have := hcyc.2
-  rw [tail_support_append, List.nodup_append] at this
+  rw [tail_support_append, List.nodup_append'] at this
   rw [isPath_def, support_eq_cons, List.nodup_cons]
   exact ⟨this.2.2 (p.end_mem_tail_support h), this.2.1⟩
 

Mathlib/Data/Fintype/Perm.lean

@@ -97,7 +97,7 @@ theorem nodup_permsOfList : ∀ {l : List α}, l.Nodup → (permsOfList l).Nodup
     have hln' : (permsOfList l).Nodup := nodup_permsOfList hl'
     have hmeml : ∀ {f : Perm α}, f ∈ permsOfList l → f a = a := fun {f} hf =>
       not_not.1 (mt (mem_of_mem_permsOfList hf) (nodup_cons.1 hl).1)
-    rw [permsOfList, List.nodup_append, List.nodup_flatMap, pairwise_iff_getElem]
+    rw [permsOfList, List.nodup_append', List.nodup_flatMap, pairwise_iff_getElem]
     refine ⟨?_, ⟨⟨?_,?_ ⟩, ?_⟩⟩
     · exact hln'
     · exact fun _ _ => hln'.map fun _ _ => mul_left_cancel

Mathlib/Data/List/Nodup.lean

@@ -176,22 +176,24 @@ theorem Nodup.of_append_left : Nodup (l₁ ++ l₂) → Nodup l₁ :=
 theorem Nodup.of_append_right : Nodup (l₁ ++ l₂) → Nodup l₂ :=
   Nodup.sublist (sublist_append_right l₁ l₂)
 
-theorem nodup_append {l₁ l₂ : List α} :
+/-- This is a variant of the `nodup_append` from the standard library,
+which does not use `Disjoint`. -/
+theorem nodup_append' {l₁ l₂ : List α} :
     Nodup (l₁ ++ l₂) ↔ Nodup l₁ ∧ Nodup l₂ ∧ Disjoint l₁ l₂ := by
   simp only [Nodup, pairwise_append, disjoint_iff_ne]
 
 theorem disjoint_of_nodup_append {l₁ l₂ : List α} (d : Nodup (l₁ ++ l₂)) : Disjoint l₁ l₂ :=
-  (nodup_append.1 d).2.2
+  (nodup_append'.1 d).2.2
 
 theorem Nodup.append (d₁ : Nodup l₁) (d₂ : Nodup l₂) (dj : Disjoint l₁ l₂) : Nodup (l₁ ++ l₂) :=
-  nodup_append.2 ⟨d₁, d₂, dj⟩
+  nodup_append'.2 ⟨d₁, d₂, dj⟩
 
 theorem nodup_append_comm {l₁ l₂ : List α} : Nodup (l₁ ++ l₂) ↔ Nodup (l₂ ++ l₁) := by
-  simp only [nodup_append, and_left_comm, disjoint_comm]
+  simp only [nodup_append', and_left_comm, disjoint_comm]
 
 theorem nodup_middle {a : α} {l₁ l₂ : List α} :
     Nodup (l₁ ++ a :: l₂) ↔ Nodup (a :: (l₁ ++ l₂)) := by
-  simp only [nodup_append, not_or, and_left_comm, and_assoc, nodup_cons, mem_append,
+  simp only [nodup_append', not_or, and_left_comm, and_assoc, nodup_cons, mem_append,
     disjoint_cons_right]
 
 theorem Nodup.of_map (f : α → β) {l : List α} : Nodup (map f l) → Nodup l :=

Mathlib/Data/Multiset/UnionInter.lean

@@ -366,7 +366,7 @@ section Nodup
 variable {s t : Multiset α} {a : α}
 
 theorem nodup_add {s t : Multiset α} : Nodup (s + t) ↔ Nodup s ∧ Nodup t ∧ Disjoint s t :=
-  Quotient.inductionOn₂ s t fun _ _ => by simp [nodup_append]
+  Quotient.inductionOn₂ s t fun _ _ => by simp [nodup_append, disjoint_iff_ne]
 
 theorem disjoint_of_nodup_add {s t : Multiset α} (d : Nodup (s + t)) : Disjoint s t :=
   (nodup_add.1 d).2.2

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6591fde7e1cd997089b617bcc11c209ea83236a6",
+   "rev": "535804a65d81e5dee7319be86c548ac649e8c047",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-15
+leanprover/lean4:nightly-2025-06-16