chore: adaptations for nightly-2025-06-30 (#8)

* 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

* chore: adaptations for nightly-2025-06-17

* chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749)

Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`.
Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633

Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Kenny Lau <[email protected]>
Co-authored-by: Fabrizio Barroero <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

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

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

* chore: adaptations for nightly-2025-06-18

* Merge master into nightly-testing

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

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

* bump Qq and batteries

* meta adaptations

* bump aesop

* fix

* fix (adaptation note)

* Update lean-toolchain for leanprover/lean4#8699

* shake

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

* fix

* Update lean-toolchain for leanprover/lean4#8699

* fix: correct memoFix's use of unsafe code

* fix: adjust noncomputable annotations for new compiler

* fix: replace use of `open private _ in` with `open private _ from`

The implementation of `open private _ from` relies on specific
internals of the old compiler and will no longer work.

* remove mul_hmul

* chore: adjust one maxHeartbeats for the new compiler

* linter

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

* chore: adaptations for nightly-2025-06-20

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

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

* fix

* fixes

* fixes

* fixes

* updated lake manifest

* comment out tests

* chore: fix for nightly-testing (leanprover-community#26246)

* fix

* fix

* fix grind typeclasses

* chore: adaptations for nightly-2025-06-20

* lake update

* Update lean-toolchain for leanprover/lean4#8914

* fix grind instance

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

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

* chore: rm unused `Lean.Util.Paths` import & use updated batteries

* Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist)

* merge lean-pr-testing-8804

* Bump dependencies and silence linter.

* Fixes

(Now `elabSimpArgs` already handles `*`, so we can delete the associated code.)

* lake update; disable unusedSimpArgs in Batteries

* lkae update aesop

* disable unusedSimpArgs in MathlibTest

* fix grind instance priorities

* comment out MathlibTest/zmod with adaptation note

* touch for CI

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

* Kick CI

* Bump batteries

* Guessing adaption for leanprover/lean4#8929

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

* fix: workflow merging master into nightly-testing

* fix

* chore: cache get uses tracking remote

* touch for new CI

* restart CI

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

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

* Teach Mathlib about `mrefine`

* Merge master into nightly-testing

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

* chore: update linter warning test outputs

* chore: remove excess line break in deprecation lint now that notes add their own line breaks

* chore: more test cleanup

* .

* cleanup adaptation notes

* fix

* fix

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* fix tests

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

* Merge master into nightly-testing

* lintining

* Merge master into nightly-testing

* unused simp args

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

* chore: adaptations for nightly-2025-06-29

* Merge master into nightly-testing

* chore: robustify `open Mathlib` benchmark

* deprecations

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

* Merge master into nightly-testing

* fixes

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

* lake update

* lake update

* lake update

* lake update

* lake update

* .

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: sgouezel <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Kenny Lau <[email protected]>
Co-authored-by: Fabrizio Barroero <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Cameron Zwarich <[email protected]>
Co-authored-by: Mac Malone <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Co-authored-by: Sebastian Graf <[email protected]>
Co-authored-by: Joseph Rotella <[email protected]>

Author: 19 people

Mathlib/Algebra/PresentedMonoid/Basic.lean

@@ -122,7 +122,7 @@ def lift : PresentedMonoid rels →* M :=
 @[to_additive]
 theorem toMonoid.unique (g : MonoidHom (conGen rels).Quotient M)
     (hg : ∀ a : α, g (of rels a) = f a) : g = lift f h :=
-  Con.lift_unique (Con.conGen_le h) g (FreeMonoid.hom_eq fun x ↦ let_fun this := hg x; this)
+  Con.lift_unique (Con.conGen_le h) g (FreeMonoid.hom_eq hg)
 
 @[to_additive (attr := simp)]
 theorem lift_of {x : α} : lift f h (of rels x) = f x := rfl

Mathlib/Analysis/Normed/Lp/PiLp.lean

@@ -818,8 +818,7 @@ protected def _root_.LinearIsometryEquiv.piLpCongrRight (e : ∀ i, α i ≃ₗ
       ≪≫ₗ (LinearEquiv.piCongrRight fun i => (e i).toLinearEquiv)
       ≪≫ₗ (WithLp.linearEquiv _ _ _).symm
   norm_map' := (WithLp.linearEquiv p 𝕜 _).symm.surjective.forall.2 fun x => by
-    simp only [LinearEquiv.trans_apply,
-      WithLp.linearEquiv_symm_apply, WithLp.linearEquiv_apply]
+    simp only [LinearEquiv.trans_apply, WithLp.linearEquiv_symm_apply, WithLp.linearEquiv_apply]
     obtain rfl | hp := p.dichotomy
     · simp_rw [PiLp.norm_toLp, Pi.norm_def, LinearEquiv.piCongrRight_apply,
         LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.nnnorm_map,

Mathlib/RingTheory/ZMod/UnitsCyclic.lean

@@ -139,7 +139,7 @@ lemma exists_one_add_mul_pow_prime_pow_eq {u v : R}
       (mul_dvd_mul_left _ hvu)
       (by
         rw [mul_pow]
-        simp only [← mul_assoc, mul_comm _ p]
+        simp only [← mul_assoc]
         rw [mul_assoc, mul_assoc, ← mul_assoc u, mul_comm u]
         apply mul_dvd_mul _ hpuv
         rw [← pow_two]
@@ -170,7 +170,7 @@ theorem orderOf_one_add_mul_prime_pow {p : ℕ} (hp : p.Prime) (m : ℕ) (hm0 :
           pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]
       · obtain ⟨y, hy⟩ := this (n + 1)
         rw [hy, ← pow_add, ← Nat.cast_pow]
-        simp [ZMod.natCast_self]
+        simp
     · rw [← pow_succ', ← pow_succ, ← pow_mul, mul_comm]
       exact pow_dvd_pow _ hpm
 
@@ -331,7 +331,7 @@ theorem isCyclic_units_iff (n : ℕ) :
   · rw [h2]; simp [isCyclic_units_two]
   by_cases h4 : n = 4
   · rw [h4]; simp [isCyclic_units_four]
-  simp only [h0, h1, h2, h4, exists_and_left, false_or, and_or_left, exists_or, ← exists_and_left]
+  simp only [h0, h1, h2, h4, false_or, and_or_left, exists_or]
   rcases (n.even_or_odd).symm with hn | hn
   · rw [isCyclic_units_iff_of_odd hn, or_iff_left]
     · congr! with p m

Mathlib/Tactic/Clean.lean

@@ -23,15 +23,13 @@ def cleanConsts : List Name :=
   [``id]
 
 /-- Clean an expression by eliminating identify functions listed in `cleanConsts`.
-Also eliminates `fun x => x` applications and tautological `let_fun` bindings. -/
+Also eliminates `fun x => x` applications and tautological `let`/`have` bindings. -/
 def clean (e : Expr) : Expr :=
   e.replace fun
     | .app (.app (.const n _) _) e' => if n ∈ cleanConsts then some e' else none
     | .app (.lam _ _ (.bvar 0) _) e' => some e'
-    | e =>
-      match e.letFun? with
-      | some (_n, _t, v, .bvar 0) => some v
-      | _ => none
+    | .letE _ _ v (.bvar 0) _ => some v
+    | _ => none
 
 end Lean.Expr
 

Mathlib/Tactic/HaveI.lean

@@ -23,7 +23,7 @@ macro_rules
   | `(assert! haveIDummy $hd:letDecl; $body) => `(haveI $hd:letDecl; $body)
 
 /--
-`haveI'` behaves like `have`, but inlines the value instead of producing a `let_fun` term.
+`haveI'` behaves like `have`, but inlines the value instead of producing a `have` term.
 
 (This is the do-notation version of the term-mode `haveI`.)
 -/
@@ -35,7 +35,7 @@ macro_rules
   | `(assert! letIDummy $hd:letDecl; $body) => `(letI $hd:letDecl; $body)
 
 /--
-`letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term.
+`letI` behaves like `let`, but inlines the value instead of producing a `let` term.
 
 (This is the do-notation version of the term-mode `haveI`.)
 -/

MathlibTest/Clean.lean

@@ -42,13 +42,13 @@ example : True := by
   guard_hyp x' :ₛ id Nat := (1 : Nat)
 
   let y := show Nat from 1
-  guard_hyp y :ₛ Nat := let_fun this := 1; this
+  guard_hyp y :ₛ Nat := have this := 1; this
   let y' := clean% show Nat from 1
   guard_hyp y' :ₛ Nat := 1
 
-  -- Not a tautological let_fun:
-  let z := clean% let_fun x := 1; x + x
-  guard_hyp z :ₛ Nat := let_fun x := 1; x + x
+  -- Not a tautological have:
+  let z := clean% have x := 1; x + x
+  guard_hyp z :ₛ Nat := have x := 1; x + x
 
   trivial
 

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "95fdabf0825b787a865d266139bbc4f86e138cbc",
+   "rev": "2eb4ccfc2628c4f68451cd73403ee2f9f29e2a9f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-28
+leanprover/lean4:nightly-2025-06-30

scripts/bench/temci-config.run.yml

@@ -27,8 +27,8 @@
       properties: ['wall-clock', 'task-clock', 'instructions:u']
     rusage_properties: ['maxrss']
     cmd: |
-      # run lake+lean like the file worker would
-      LEAN_PATH=$(lake setup-file --no-build Mathlib Mathlib | jq -r '.paths.oleanPath | join(":")') lean Mathlib.lean
+      # approximate `import Mathlib` in the editor
+      lake lean Mathlib.lean
     runs: 5
 - attributes:
     description: size