chore: adaptations for nightly-2025-06-18 (#26077)

* 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

* 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) (#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]>

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

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

---------

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

Author: 16 people

Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

@@ -269,7 +269,7 @@ instance counterUniformity : UniformSpace ℕ := UniformSpace.ofCore counterCore
 
 lemma HasBasis_counterUniformity :
     (uniformity ℕ).HasBasis (fun _ ↦ True) fundamentalEntourage := by
-  show counterCoreUniformity.uniformity.HasBasis (fun _ ↦ True) fundamentalEntourage
+  change counterCoreUniformity.uniformity.HasBasis (fun _ ↦ True) fundamentalEntourage
   simp only [Filter.hasBasis_iff, exists_and_left, true_and]
   intro T
   refine ⟨fun ⟨s, ⟨⟨r, hr⟩, hs⟩⟩ ↦ ⟨r, subset_of_eq_of_subset hr hs⟩ , fun ⟨n, hn⟩ ↦ ?_⟩
@@ -292,7 +292,7 @@ theorem TopIsDiscrete' : DiscreteTopology ℕ := by
     rw [mem_fundamentalEntourage]
     aesop
   · refine ⟨fundamentalEntourage (n + 1), ?_, ?_⟩
-    · show fundamentalEntourage (n + 1) ∈ counterCoreUniformity.uniformity
+    · change fundamentalEntourage (n + 1) ∈ counterCoreUniformity.uniformity
       exact @Filter.HasBasis.mem_of_mem (ℕ × ℕ) ℕ counterCoreUniformity.uniformity (fun _ ↦ True)
         fundamentalEntourage (n + 1) HasBasis_counterUniformity trivial
     · simp only [preimage_subset_iff, mem_fundamentalEntourage, add_le_iff_nonpos_right,

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -154,7 +154,7 @@ protected def copy (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) :
     NonUnitalSubalgebra R A :=
   { S.toNonUnitalSubsemiring.copy s hs with
     smul_mem' := fun r a (ha : a ∈ s) => by
-      show r • a ∈ s
+      change r • a ∈ s
       rw [hs] at ha ⊢
       exact S.smul_mem' r ha }
 
@@ -673,7 +673,7 @@ lemma adjoin_eq_span (s : Set A) : (adjoin R s).toSubmodule = span R (Subsemigro
       case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
     | smul r x _ hpx => exact smul_mem _ _ hpx
   · apply span_le.2 _
-    show Subsemigroup.closure s ≤ (adjoin R s).toSubsemigroup
+    change Subsemigroup.closure s ≤ (adjoin R s).toSubsemigroup
     exact Subsemigroup.closure_le.2 (subset_adjoin R)
 
 variable (R A)

Mathlib/Algebra/Algebra/Operations.lean

@@ -437,7 +437,7 @@ theorem map_op_mul :
   · simp_rw [map_le_iff_le_comap]
     refine mul_le.2 fun m hm n hn => ?_
     rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]
-    show op n * op m ∈ _
+    change op n * op m ∈ _
     exact mul_mem_mul hn hm
   · refine mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => ?_)
     rw [Submodule.mem_map_equiv] at hm hn ⊢

Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

@@ -49,7 +49,7 @@ theorem mem_of_finset_sum_eq_one_of_pow_smul_mem
   let l' : ι → S' := fun x => ⟨l x, hl x⟩
   have e' : ∑ i ∈ ι', l' i * s' i = 1 := by
     ext
-    show S'.subtype (∑ i ∈ ι', l' i * s' i) = 1
+    change S'.subtype (∑ i ∈ ι', l' i * s' i) = 1
     simpa only [map_sum, map_mul] using e
   have : Ideal.span (s' '' ι') = ⊤ := by
     rw [Ideal.eq_top_iff_one, ← e']

Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

@@ -24,7 +24,7 @@ theorem mul_toSubmodule_le (S T : Subalgebra R A) :
     (Subalgebra.toSubmodule S)* (Subalgebra.toSubmodule T) ≤ Subalgebra.toSubmodule (S ⊔ T) := by
   rw [Submodule.mul_le]
   intro y hy z hz
-  show y * z ∈ S ⊔ T
+  change y * z ∈ S ⊔ T
   exact mul_mem (Algebra.mem_sup_left hy) (Algebra.mem_sup_right hz)
 
 /-- As submodules, subalgebras are idempotent. -/

Mathlib/Algebra/Algebra/Unitization.lean

@@ -562,12 +562,12 @@ instance instAlgebra : Algebra S (Unitization R A) where
   commutes' := fun s x => by
     induction x with
     | inl_add_inr =>
-      show inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
+      change inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
       rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]
   smul_def' := fun s x => by
     induction x with
     | inl_add_inr =>
-      show _ = inl (algebraMap S R s) * _
+      change _ = inl (algebraMap S R s) * _
       rw [mul_add, smul_add,Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
         smul_one_mul, inl_smul, inr_smul, smul_one_smul]
 

Mathlib/Algebra/Algebra/ZMod.lean

@@ -31,7 +31,7 @@ abbrev algebra' (h : m ∣ n) : Algebra (ZMod n) R where
   commutes' := fun a r =>
     show (cast a * r : R) = r * cast a by
       rcases ZMod.intCast_surjective a with ⟨k, rfl⟩
-      show ZMod.castHom h R k * r = r * ZMod.castHom h R k
+      change ZMod.castHom h R k * r = r * ZMod.castHom h R k
       rw [map_intCast, Int.cast_comm]
   smul_def' := fun _ _ => rfl
 

Mathlib/Algebra/BigOperators/Fin.lean

@@ -717,7 +717,7 @@ theorem alternatingProd_eq_finset_prod {G : Type*} [DivisionCommMonoid G] :
     rw [alternatingProd, Finset.prod_eq_one]
     rintro ⟨i, ⟨⟩⟩
   | g::[] => by
-    show g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)
+    change g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)
     rw [Fin.prod_univ_succ]; simp
   | g::h::L =>
     calc g * h⁻¹ * L.alternatingProd

Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

@@ -179,7 +179,7 @@ instance : (forget₂ (TopModuleCat R) TopCat).ReflectsIsomorphisms where
   reflects {X Y} f hf := by
     let e : X ≃L[R] Y :=
       { __ := f.hom, __ := TopCat.homeoOfIso (asIso ((forget₂ (TopModuleCat R) TopCat).map f)) }
-    show IsIso (ofIso e).hom
+    change IsIso (ofIso e).hom
     infer_instance
 
 @[simp]
@@ -230,7 +230,7 @@ def isColimit {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
     refine sInf_le ⟨continuousSMul_induced (M₂ := s.pt) (hc.desc ((forget₂ _ _).mapCocone s)).hom,
       continuousAdd_induced (N := s.pt) (hc.desc ((forget₂ _ _).mapCocone s)).hom, fun i ↦ ?_⟩
     rw [coinduced_le_iff_le_induced, induced_compose, ← continuous_iff_le_induced]
-    show Continuous (X := F.obj i) (Y := s.pt)
+    change Continuous (X := F.obj i) (Y := s.pt)
       (c.ι.app i ≫ hc.desc ((forget₂ _ (ModuleCat R)).mapCocone s)).hom
     rw [hc.fac]
     exact (s.ι.app i).hom.2⟩
@@ -290,7 +290,7 @@ def isLimit {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
     rw [continuous_iff_coinduced_le]
     refine le_iInf fun i ↦ ?_
     rw [coinduced_le_iff_le_induced, induced_compose, ← continuous_iff_le_induced]
-    show Continuous (X := s.pt) (Y := F.obj i)
+    change Continuous (X := s.pt) (Y := F.obj i)
       (hc.lift ((forget₂ _ (ModuleCat R)).mapCone s) ≫ c.π.app i).hom
     rw [hc.fac]
     exact (s.π.app i).hom.2⟩

Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean

@@ -94,7 +94,7 @@ instance : CategoryWithHomology (TopModuleCat R) := by
   let F := ShortComplex.leftRightHomologyComparison' D₁ D₂
   suffices IsIso F from ⟨⟨.ofIsIsoLeftRightHomologyComparison' D₁ D₂⟩⟩
   have hF : Function.Bijective F := by
-    show Function.Bijective ((forget₂ _ (ModuleCat R)).map F)
+    change Function.Bijective ((forget₂ _ (ModuleCat R)).map F)
     rw [← ConcreteCategory.isIso_iff_bijective, ShortComplex.map_leftRightHomologyComparison']
     infer_instance
   have hF' : Topology.IsEmbedding F := by