chore: adaptations for nightly-2025-06-28 (#5)

* 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

* 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

* lint

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: github-actions <[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

Archive/Arithcc.lean

@@ -281,8 +281,7 @@ theorem compiler_correctness
   -- 5.III
   | sum =>
     rename_i e_s₁ e_s₂ e_ih_s₁ e_ih_s₂
-    simp only [compile, List.append_assoc, List.singleton_append, List.cons_append, outcome_append,
-      outcome, value]
+    simp only [compile, List.append_assoc, List.cons_append, outcome_append, outcome, value]
     generalize value e_s₁ ξ = ν₁ at e_ih_s₁ ⊢
     generalize value e_s₂ ξ = ν₂ at e_ih_s₂ ⊢
     generalize dν : ν₁ + ν₂ = ν

Archive/Examples/Eisenstein.lean

@@ -63,7 +63,7 @@ example : Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℤ[X]) := by
       rw [pow_two, ← sub_mul]
       apply dvd_mul_left
     · symm
-      simp only [modByMonicHom_apply, Polynomial.modByMonic_eq_self_iff hq_monic, f]
+      simp only [modByMonicHom_apply, Polynomial.modByMonic_eq_self_iff hq_monic]
       rw [show q.degree = 2 by unfold q; compute_degree!]
       rw [show degree _ = 0 by compute_degree!]
       norm_num

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -109,8 +109,7 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
             obtain ⟨⟨⟨en, ec⟩, er⟩, ed⟩ := he₂
             split at b <;> rename_i h'
             · subst h'; simp_all
-            · simp_all only [ne_eq, vars, List.singleton_append, List.cons_append,
-                Bool.not_eq_true, List.mem_cons, List.mem_append, false_or]
+            · simp_all only [vars, List.cons_append, List.mem_cons, List.mem_append, false_or]
               cases b <;> simp_all⟩
     | some b =>
       have ⟨e', he'⟩ := normalize' l (.ite (lit b) t e)

Archive/Imo/Imo1972Q5.lean

@@ -37,7 +37,7 @@ theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y
   -- Show that `2 * (‖f x‖ * ‖g y‖) ≤ 2 * k`.
   have hk₂ : ∀ x, 2 * (‖f x‖ * ‖g y‖) ≤ 2 * k := fun x ↦
     calc
-      2 * (‖f x‖ * ‖g y‖) = ‖2 * f x * g y‖ := by simp [abs_mul, mul_assoc]
+      2 * (‖f x‖ * ‖g y‖) = ‖2 * f x * g y‖ := by simp [mul_assoc]
       _ = ‖f (x + y) + f (x - y)‖ := by rw [hf1]
       _ ≤ ‖f (x + y)‖ + ‖f (x - y)‖ := norm_add_le _ _
       _ ≤ k + k := add_le_add (hk₁ _) (hk₁ _)
@@ -93,7 +93,7 @@ theorem imo1972_q5' (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x -
     suffices 2 * (‖f x‖ * ‖g y‖) ≤ 2 * k by
       rwa [le_div_iff₀ hgy, ← mul_le_mul_left (zero_lt_two : (0 : ℝ) < 2)]
     calc
-      2 * (‖f x‖ * ‖g y‖) = ‖2 * f x * g y‖ := by simp [abs_mul, mul_assoc]
+      2 * (‖f x‖ * ‖g y‖) = ‖2 * f x * g y‖ := by simp [mul_assoc]
       _ = ‖f (x + y) + f (x - y)‖ := by rw [hf1]
       _ ≤ ‖f (x + y)‖ + ‖f (x - y)‖ := abs_add _ _
       _ ≤ 2 * k := by linarith [h (x + y), h (x - y)]

Archive/Imo/Imo1975Q1.lean

@@ -36,7 +36,7 @@ theorem imo1975_q1 (hσ : {x | σ x ≠ x} ⊆ Finset.Icc 1 n)
     rw [← Equiv.Perm.sum_comp σ (Finset.Icc 1 n) _ hσ]
   -- let's cancel terms appearing on both sides
   rw [hσy, add_le_add_iff_right, sub_le_sub_iff_left]
-  simp only [gt_iff_lt, Nat.lt_one_iff, mul_assoc, ← Finset.mul_sum, zero_lt_two, mul_le_mul_left]
+  simp only [mul_assoc, ← Finset.mul_sum, zero_lt_two, mul_le_mul_left]
   -- what's left to prove is a version of the rearrangement inequality
   apply MonovaryOn.sum_mul_comp_perm_le_sum_mul _ hσ
   -- finally we need to show that `x` and `y` 'vary' together on `[1, n]` and this is due to both of

Archive/Imo/Imo1987Q1.lean

@@ -79,7 +79,7 @@ def fixedPointsEquiv' :
     ⟨⟨card (fixedPoints p.1.2), (card_subtype_le _).trans_lt (Nat.lt_succ_self _)⟩, ⟨p.1.2, rfl⟩,
       ⟨p.1.1, p.2⟩⟩
   left_inv := fun ⟨⟨k, hk⟩, ⟨σ, hσ⟩, ⟨x, hx⟩⟩ => by
-    simp only [mem_fiber, Fin.val_mk] at hσ
+    simp only [mem_fiber] at hσ
     subst k; rfl
   right_inv := fun ⟨⟨x, σ⟩, h⟩ => rfl
 

Archive/Imo/Imo1994Q1.lean

@@ -78,7 +78,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : #A = m + 1)
     intro x hx
     simp only [Equiv.subLeft_apply, a, rev] at h
     simp only [mem_map, mem_Icc, mem_Ioc, Fin.zero_le, true_and, Equiv.subLeft_apply,
-      Function.Embedding.coeFn_mk, exists_prop, RelEmbedding.coe_toEmbedding, f, rev] at hx ⊢
+      Function.Embedding.coeFn_mk, RelEmbedding.coe_toEmbedding, f, rev] at hx ⊢
     rcases hx with ⟨i, ⟨hi, rfl⟩⟩
     have h1 : a i + a (Fin.last m - k) ≤ n := by unfold a; linarith only [h, a.monotone hi]
     have h2 : a i + a (Fin.last m - k) ∈ A := hadd _ (ha _) _ (ha _) h1

Archive/Imo/Imo1998Q2.lean

@@ -106,7 +106,7 @@ theorem A_fibre_over_contestant (c : C) :
     (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct) =
       ((A r).filter fun a : AgreedTriple C J => a.contestant = c).image Prod.snd := by
   ext p
-  simp only [A, Finset.mem_univ, Finset.mem_filter, Finset.mem_image, exists_prop]
+  simp only [A, Finset.mem_univ, Finset.mem_filter, Finset.mem_image]
   constructor
   · rintro ⟨_, h₂⟩; refine ⟨(c, p), ?_⟩; tauto
   · intro h; aesop
@@ -231,7 +231,7 @@ theorem imo1998_q2 [Fintype J] [Fintype C] (a b k : ℕ) (hC : Fintype.card C =
   -- We are now essentially done; we just need to bash `h` into exactly the right shape.
   have hl : k * ((2 * z + 1) * (2 * z + 1) - (2 * z + 1)) = k * (2 * (2 * z + 1)) * z := by
     have : 0 < 2 * z + 1 := by aesop
-    simp only [mul_comm, add_mul, one_mul, nonpos_iff_eq_zero, add_tsub_cancel_right]; ring
+    simp only [mul_comm, add_mul, one_mul, add_tsub_cancel_right]; ring
   have hr : 2 * z * z * a = 2 * z * a * z := by ring
   rw [hl, hr] at h
   rcases z with - | z

Archive/Imo/Imo2006Q5.lean

@@ -171,7 +171,7 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
     replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
     rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
     simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.def,
-      eval_sub, eval_add, eval_X, eval_C, eval_intCast, Int.cast_id, zero_add]
+      eval_sub, eval_add, eval_X, eval_intCast, Int.cast_id, zero_add]
     -- An auxiliary lemma proved earlier implies we only need to show |t - a| = |u - b| and
     -- |t - b| = |u - a|. We prove this by establishing that each side of either equation divides
     -- the other.

Archive/Imo/Imo2008Q3.lean

@@ -40,7 +40,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
   let n := Int.natAbs m
   have hnat₁ : p ∣ n ^ 2 + 1 := by
     refine Int.natCast_dvd_natCast.mp ?_
-    simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.natCast_succ, Int.natCast_dvd_natCast.mp]
+    simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.natCast_succ]
     refine (ZMod.intCast_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp ?_
     simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
     rw [pow_two, ← hy]; exact neg_add_cancel 1