diff --git a/Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean b/Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean
index 36cb59bd12e..7bd64f48a5c 100644
--- a/Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean
+++ b/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,
diff --git a/Mathlib/Algebra/Group/Hom/Basic.lean b/Mathlib/Algebra/Group/Hom/Basic.lean
index afb4e73e22c..f0193a2c9cf 100644
--- a/Mathlib/Algebra/Group/Hom/Basic.lean
+++ b/Mathlib/Algebra/Group/Hom/Basic.lean
@@ -77,6 +77,7 @@ instance [Mul M] [CommSemigroup N] : Mul (M →ₙ* N) :=
   ⟨fun f g =>
     { toFun := fun m => f m * g m,
       map_mul' := fun x y => by
+        show f (x * y) * g (x * y) = f x * g x * (f y * g y)
         rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)] }⟩

 @[to_additive (attr := simp)]
diff --git a/Mathlib/AlgebraicGeometry/Gluing.lean b/Mathlib/AlgebraicGeometry/Gluing.lean
index 642b1941df8..04153c33d3c 100644
--- a/Mathlib/AlgebraicGeometry/Gluing.lean
+++ b/Mathlib/AlgebraicGeometry/Gluing.lean
@@ -755,7 +755,7 @@ def openCover : (colimit F).OpenCover :=
     fun i ↦ (glueData F).openCover).copy J F.obj (colimit.ι F)
     ((equivShrink J).trans <| (Equiv.uniqueSigma fun (_ : Unit) ↦ Shrink J).symm)
     (fun _ ↦ F.mapIso (eqToIso (by simp [GlueData.openCover, glueData]))) fun i ↦ by
-  show colimit.ι F i = _ ≫ (glueData F).ι (equivShrink J i) ≫ _
+  change colimit.ι F i = _ ≫ (glueData F).ι (equivShrink J i) ≫ _
   simp [← Category.assoc, ← Iso.comp_inv_eq, cocone]

 @[simp] lemma openCover_J : (openCover F).J = J := rfl
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean b/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
index 3242e5cdb86..bd4edd1135c 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
@@ -80,7 +80,8 @@ instance : IsLocalAtTarget @IsSeparated := by
 instance (R S : CommRingCat.{u}) (f : R ⟶ S) : IsSeparated (Spec.map f) := by
   constructor
   letI := f.hom.toAlgebra
-  show IsClosedImmersion (Limits.pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap R S))))
+  show IsClosedImmersion
+    (Limits.pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap R S))))
   rw [diagonal_Spec_map, MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion]
   exact .spec_of_surjective _ fun x ↦ ⟨.tmul R 1 x,
     (Algebra.TensorProduct.lmul'_apply_tmul (R := R) (S := S) 1 x).trans (one_mul x)⟩
diff --git a/Mathlib/Analysis/Normed/Module/Basic.lean b/Mathlib/Analysis/Normed/Module/Basic.lean
index 2dd352ce9d8..43525a96f0b 100644
--- a/Mathlib/Analysis/Normed/Module/Basic.lean
+++ b/Mathlib/Analysis/Normed/Module/Basic.lean
@@ -512,15 +512,18 @@ abbrev PseudoMetricSpace.ofSeminormedSpaceCore {𝕜 E : Type*} [NormedField
     PseudoMetricSpace E where
   dist x y := ‖x - y‖
   dist_self x := by
+    show ‖x - x‖ = 0
     simp only [sub_self]
     have : (0 : E) = (0 : 𝕜) • (0 : E) := by simp
     rw [this, core.norm_smul]
     simp
   dist_comm x y := by
+    show ‖x - y‖ = ‖y - x‖
     have : y - x = (-1 : 𝕜) • (x - y) := by simp
     rw [this, core.norm_smul]
     simp
   dist_triangle x y z := by
+    show ‖x - z‖ ≤ ‖x - y‖ + ‖y - z‖
     have : x - z = (x - y) + (y - z) := by abel
     rw [this]
     exact core.norm_triangle _ _
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
index 85855b87b3c..a1d6527ce13 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
@@ -251,7 +251,8 @@ theorem abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) :
 theorem hasSum_pow_div_log_of_abs_lt_one {x : ℝ} (h : |x| < 1) :
     HasSum (fun n : ℕ => x ^ (n + 1) / (n + 1)) (-log (1 - x)) := by
   rw [Summable.hasSum_iff_tendsto_nat]
-  · rw [tendsto_iff_norm_sub_tendsto_zero]
+  · show Tendsto (fun n : ℕ => ∑ i ∈ range n, x ^ (i + 1) / (i + 1)) atTop (𝓝 (-log (1 - x)))
+    rw [tendsto_iff_norm_sub_tendsto_zero]
     simp only [norm_eq_abs, sub_neg_eq_add]
     refine squeeze_zero (fun n => abs_nonneg _) (abs_log_sub_add_sum_range_le h) ?_
     suffices Tendsto (fun t : ℕ => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|))) by
diff --git a/Mathlib/Data/Multiset/Fold.lean b/Mathlib/Data/Multiset/Fold.lean
index 39cddc1ec4c..01320a027a2 100644
--- a/Mathlib/Data/Multiset/Fold.lean
+++ b/Mathlib/Data/Multiset/Fold.lean
@@ -90,6 +90,7 @@ theorem fold_dedup_idem [DecidableEq α] [hi : Std.IdempotentOp op] (s : Multise
     (dedup s).fold op b = s.fold op b :=
   Multiset.induction_on s (by simp) fun a s IH => by
     by_cases h : a ∈ s <;> simp [IH, h]
+    show fold op b s = op a (fold op b s)
     rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]

 end Fold
diff --git a/Mathlib/Data/Nat/Pairing.lean b/Mathlib/Data/Nat/Pairing.lean
index 620cf915a8d..d95ffce65e2 100644
--- a/Mathlib/Data/Nat/Pairing.lean
+++ b/Mathlib/Data/Nat/Pairing.lean
@@ -59,9 +59,11 @@ alias pair_unpair' := pair_eq_of_unpair_eq
 @[simp]
 theorem unpair_pair (a b : ℕ) : unpair (pair a b) = (a, b) := by
   dsimp only [pair]; split_ifs with h
-  · have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))
+  · show unpair (b * b + a) = (a, b)
+    have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))
     simp [unpair, be, Nat.add_sub_cancel_left, h]
-  · have ae : sqrt (a * a + (a + b)) = a := by
+  · show unpair (a * a + a + b) = (a, b)
+    have ae : sqrt (a * a + (a + b)) = a := by
       rw [sqrt_add_eq]
       exact Nat.add_le_add_left (le_of_not_gt h) _
     simp [unpair, ae, Nat.not_lt_zero, Nat.add_assoc, Nat.add_sub_cancel_left]
diff --git a/Mathlib/Data/PFun.lean b/Mathlib/Data/PFun.lean
index 110e5223619..e0454d970c9 100644
--- a/Mathlib/Data/PFun.lean
+++ b/Mathlib/Data/PFun.lean
@@ -439,6 +439,7 @@ theorem preimage_asSubtype (f : α →. β) (s : Set β) :
     f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s := by
   ext x
   simp only [Set.mem_preimage, Set.mem_setOf_eq, PFun.asSubtype, PFun.mem_preimage]
+  show f.fn x.val _ ∈ s ↔ ∃ y ∈ s, y ∈ f x.val
   exact
     Iff.intro (fun h => ⟨_, h, Part.get_mem _⟩) fun ⟨y, ys, fxy⟩ =>
       have : f.fn x.val x.property ∈ f x.val := Part.get_mem _
diff --git a/Mathlib/FieldTheory/ChevalleyWarning.lean b/Mathlib/FieldTheory/ChevalleyWarning.lean
index 1be6e67ca26..38842b958a9 100644
--- a/Mathlib/FieldTheory/ChevalleyWarning.lean
+++ b/Mathlib/FieldTheory/ChevalleyWarning.lean
@@ -139,6 +139,7 @@ theorem char_dvd_card_solutions_of_sum_lt {s : Finset ι} {f : ι → MvPolynomi
   -- We are now ready to apply the main machine, proven before.
   apply F.sum_eval_eq_zero
   -- It remains to verify the crucial assumption of this machine
+  show F.totalDegree < (q - 1) * Fintype.card σ
   calc
     F.totalDegree ≤ ∑ i ∈ s, (1 - f i ^ (q - 1)).totalDegree := totalDegree_finset_prod s _
     _ ≤ ∑ i ∈ s, (q - 1) * (f i).totalDegree := sum_le_sum fun i _ => ?_
diff --git a/Mathlib/GroupTheory/CoprodI.lean b/Mathlib/GroupTheory/CoprodI.lean
index 58451706555..81657588017 100644
--- a/Mathlib/GroupTheory/CoprodI.lean
+++ b/Mathlib/GroupTheory/CoprodI.lean
@@ -1000,8 +1000,10 @@ theorem _root_.FreeGroup.injective_lift_of_ping_pong : Function.Injective (FreeG
   let f : ∀ i, H i →* G := fun i => FreeGroup.lift fun _ => a i
   let X' : ι → Set α := fun i => X i ∪ Y i
   apply lift_injective_of_ping_pong f _ X'
-  · exact fun i => Set.Nonempty.inl (hXnonempty i)
-  · intro i j hij
+  · show ∀ i, (X' i).Nonempty
+    exact fun i => Set.Nonempty.inl (hXnonempty i)
+  · show Pairwise (Disjoint on X')
+    intro i j hij
     simp only [X']
     apply Disjoint.union_left <;> apply Disjoint.union_right
     · exact hXdisj hij
diff --git a/Mathlib/GroupTheory/Coxeter/Inversion.lean b/Mathlib/GroupTheory/Coxeter/Inversion.lean
index d1bf4669bd9..765db89953b 100644
--- a/Mathlib/GroupTheory/Coxeter/Inversion.lean
+++ b/Mathlib/GroupTheory/Coxeter/Inversion.lean
@@ -412,6 +412,7 @@ theorem prod_leftInvSeq (ω : List B) : prod (lis ω) = (π ω)⁻¹ := by
 theorem IsReduced.nodup_rightInvSeq {ω : List B} (rω : cs.IsReduced ω) : List.Nodup (ris ω) := by
   apply List.nodup_iff_getElem?_ne_getElem?.mpr
   intro j j' j_lt_j' j'_lt_length (dup : (rightInvSeq cs ω)[j]? = (rightInvSeq cs ω)[j']?)
+  show False
   replace j'_lt_length : j' < List.length ω := by simpa using j'_lt_length
   rw [getElem?_eq_getElem (by simp; omega), getElem?_eq_getElem (by simp; omega)] at dup
   apply Option.some_injective at dup
diff --git a/Mathlib/GroupTheory/Sylow.lean b/Mathlib/GroupTheory/Sylow.lean
index be5d53fbaf1..52fcb8c4998 100644
--- a/Mathlib/GroupTheory/Sylow.lean
+++ b/Mathlib/GroupTheory/Sylow.lean
@@ -115,6 +115,7 @@ def comapOfKerIsPGroup (hϕ : IsPGroup p ϕ.ker) (h : P ≤ ϕ.range) : Sylow p
   { P.1.comap ϕ with
     isPGroup' := P.2.comap_of_ker_isPGroup ϕ hϕ
     is_maximal' := fun {Q} hQ hle => by
+      show Q = P.1.comap ϕ
       rw [← P.3 (hQ.map ϕ) (le_trans (ge_of_eq (map_comap_eq_self h)) (map_mono hle))]
       exact (comap_map_eq_self ((P.1.ker_le_comap ϕ).trans hle)).symm }

@@ -607,6 +608,8 @@ theorem exists_subgroup_card_pow_succ [Finite G] {p : ℕ} {n : ℕ} [hp : Fact
   have hequiv : H ≃ H.subgroupOf H.normalizer := (subgroupOfEquivOfLe le_normalizer).symm.toEquiv
   ⟨Subgroup.map (normalizer H).subtype
       (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x)), by
+    show Nat.card (Subgroup.map H.normalizer.subtype
+              (comap (mk' (H.subgroupOf H.normalizer)) (Subgroup.zpowers x))) = p ^ (n + 1)
     suffices Nat.card (Subtype.val ''
               (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x) : Set H.normalizer)) =
         p ^ (n + 1)
diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean
index d4ebd019767..0fe902b3b08 100644
--- a/Mathlib/Init.lean
+++ b/Mathlib/Init.lean
@@ -78,6 +78,7 @@ register_linter_set linter.mathlibStandardSet :=
   linter.style.openClassical
   linter.style.missingEnd
   linter.style.setOption
+  linter.style.show
   linter.style.maxHeartbeats
   -- The `docPrime` linter is disabled: https://github.com/leanprover-community/mathlib4/issues/20560

diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
index 6726d3457a9..c69fb47605e 100644
--- a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
+++ b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
@@ -6,3 +6,4 @@ Authors: Amelia Livingston
 import Mathlib.RepresentationTheory.Homological.Resolution

 deprecated_module (since := "2025-06-14")
+
diff --git a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean
index ec3672b51c1..8395edb19a9 100644
--- a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean
+++ b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean
@@ -205,7 +205,7 @@ alias cochainsMap_f_1_comp_oneCochainsLequiv := cochainsMap_f_1_comp_oneCochains
 lemma cochainsMap_f_2_comp_twoCochainsIso :
     (cochainsMap f φ).f 2 ≫ (twoCochainsIso B).hom = (twoCochainsIso A).hom ≫ fTwo f φ := by
   ext x g
-  show φ.hom (x _) = φ.hom (x _)
+  change φ.hom (x _) = φ.hom (x _)
   rcongr x
   fin_cases x <;> rfl

@@ -216,7 +216,7 @@ alias cochainsMap_f_2_comp_twoCochainsLequiv := cochainsMap_f_2_comp_twoCochains
 lemma cochainsMap_f_3_comp_threeCochainsIso :
     (cochainsMap f φ).f 3 ≫ (threeCochainsIso B).hom = (threeCochainsIso A).hom ≫ fThree f φ := by
   ext x g
-  show φ.hom (x _) = φ.hom (x _)
+  change φ.hom (x _) = φ.hom (x _)
   rcongr x
   fin_cases x <;> rfl

diff --git a/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean b/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
index c9af56ad7d7..e6a028c5401 100644
--- a/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
+++ b/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
@@ -167,7 +167,7 @@ theorem comp_dZero_eq :
     (zeroCochainsIso A).hom ≫ dZero A =
       (inhomogeneousCochains A).d 0 1 ≫ (oneCochainsIso A).hom := by
   ext x y
-  show A.ρ y (x default) - x default = _ + ({0} : Finset _).sum _
+  change A.ρ y (x default) - x default = _ + ({0} : Finset _).sum _
   simp_rw [Fin.val_eq_zero, zero_add, pow_one, neg_smul, one_smul,
     Finset.sum_singleton, sub_eq_add_neg]
   rcongr i <;> exact Fin.elim0 i
@@ -197,7 +197,7 @@ theorem comp_dOne_eq :
     (oneCochainsIso A).hom ≫ dOne A =
       (inhomogeneousCochains A).d 1 2 ≫ (twoCochainsIso A).hom := by
   ext x y
-  show A.ρ y.1 (x _) - x _ + x _ =  _ + _
+  change A.ρ y.1 (x _) - x _ + x _ =  _ + _
   rw [Fin.sum_univ_two]
   simp only [Fin.val_zero, zero_add, pow_one, neg_smul, one_smul, Fin.val_one,
     Nat.one_add, neg_one_sq, sub_eq_add_neg, add_assoc]
@@ -228,7 +228,7 @@ theorem comp_dTwo_eq :
     (twoCochainsIso A).hom ≫ dTwo A =
       (inhomogeneousCochains A).d 2 3 ≫ (threeCochainsIso A).hom := by
   ext x y
-  show A.ρ y.1 (x _) - x _ + x _ - x _ = _ + _
+  change A.ρ y.1 (x _) - x _ + x _ - x _ = _ + _
   dsimp
   rw [Fin.sum_univ_three]
   simp only [sub_eq_add_neg, add_assoc, Fin.val_zero, zero_add, pow_one, neg_smul,
diff --git a/Mathlib/RepresentationTheory/Homological/Resolution.lean b/Mathlib/RepresentationTheory/Homological/Resolution.lean
index db6eda42b9c..214b52ab6d9 100644
--- a/Mathlib/RepresentationTheory/Homological/Resolution.lean
+++ b/Mathlib/RepresentationTheory/Homological/Resolution.lean
@@ -138,7 +138,7 @@ def ofMulActionBasisAux :
         show (r * x) ⊗ₜ y = _
         rw [← ofMulAction_self_smul_eq_mul, smul_tprod_one_asModule]
       · rw [smul_add, hz, hy, smul_add] -/
-      show _ = Representation.asAlgebraHom (tensorObj (Rep.leftRegular k G)
+      change _ = Representation.asAlgebraHom (tensorObj (Rep.leftRegular k G)
         (Rep.trivial k G ((Fin n → G) →₀ k))).ρ r _
       refine x.induction_on ?_ (fun x y => ?_) fun y z hy hz => ?_
       · rw [smul_zero, map_zero]
@@ -335,10 +335,10 @@ a trivial `G`-representation, and the complex which is `k` at 0 and 0 everywhere
 theorem forget₂ToModuleCatHomotopyEquiv_f_0_eq :
     (forget₂ToModuleCatHomotopyEquiv k G).1.f 0 = (forget₂ (Rep k G) _).map (ε k G) := by
   refine ModuleCat.hom_ext <| Finsupp.lhom_ext fun (x : Fin 1 → G) r => ?_
-  show mapDomain _ _ _ = Finsupp.linearCombination _ _ _
+  change mapDomain _ _ _ = Finsupp.linearCombination _ _ _
   simp only [HomotopyEquiv.ofIso, Iso.symm_hom, compForgetAugmented, compForgetAugmentedIso,
     eqToIso.inv, HomologicalComplex.eqToHom_f]
-  show mapDomain _ (single x r) _ = _
+  change mapDomain _ (single x r) _ = _
   simp [Unique.eq_default (terminal.from _), single_apply, if_pos (Subsingleton.elim _ _)]

 theorem d_comp_ε : (standardComplex k G).d 1 0 ≫ ε k G = 0 := by
diff --git a/Mathlib/RingTheory/HahnSeries/Lex.lean b/Mathlib/RingTheory/HahnSeries/Lex.lean
index 100f0485430..1adff1771c6 100644
--- a/Mathlib/RingTheory/HahnSeries/Lex.lean
+++ b/Mathlib/RingTheory/HahnSeries/Lex.lean
@@ -143,7 +143,7 @@ theorem order_abs [Zero Γ] (x : Lex (HahnSeries Γ R)) : (ofLex |x|).order = (o
   · simp
   · have hne' : ofLex x ≠ 0 := hne
     have habs : ofLex |x| ≠ 0 := by
-      show |x| ≠ 0
+      change |x| ≠ 0
       simpa using hne
     apply WithTop.coe_injective
     rw [order_eq_orderTop_of_ne habs, order_eq_orderTop_of_ne hne']
diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean
index 18da51dfd8a..d61a1a7d8b5 100644
--- a/Mathlib/Tactic/Linter/Style.lean
+++ b/Mathlib/Tactic/Linter/Style.lean
@@ -5,6 +5,7 @@ Authors: Michael Rothgang
 -/

 import Lean.Elab.Command
+import Lean.Server.InfoUtils
 -- Import this linter explicitly to ensure that
 -- this file has a valid copyright header and module docstring.
 import Mathlib.Tactic.Linter.Header
@@ -34,6 +35,7 @@ This file defines the following linters:
 - the `longLine` linter checks for lines which have more than 100 characters
 - the `openClassical` linter checks for `open (scoped) Classical` statements which are not
   scoped to a single declaration
+- the `show` linter checks for `show`s that change the goal and should be replaced by `change`

 All of these linters are enabled in mathlib by default, but disabled globally
 since they enforce conventions which are inherently subjective.
@@ -464,7 +466,7 @@ register_option linter.style.nameCheck : Bool := {
 namespace Style.nameCheck

 @[inherit_doc linter.style.nameCheck]
-def doubleUnderscore: Linter where run := withSetOptionIn fun stx => do
+def doubleUnderscore : Linter where run := withSetOptionIn fun stx => do
     unless getLinterValue linter.style.nameCheck (← getLinterOptions) do
       return
     if (← get).messages.hasErrors then
@@ -537,4 +539,47 @@ initialize addLinter openClassicalLinter

 end Style.openClassical

+/-! # The "show" linter -/
+
+/--
+The "show" linter emits a warning if the `show` tactic changed the goal. `show` should only be used
+to indicate intermediate goal states for proof readability. When the goal is actually changed,
+`change` should be preferred.
+-/
+register_option linter.style.show : Bool := {
+  defValue := false
+  descr := "enable the show linter"
+}
+
+namespace Style.show
+
+@[inherit_doc Mathlib.Linter.linter.style.show]
+def showLinter : Linter where run := withSetOptionIn fun stx => do
+    unless getLinterValue linter.style.show (← getLinterOptions) do
+      return
+    if (← get).messages.hasErrors then
+      return
+    for tree in (← getInfoTrees) do
+      tree.foldInfoM (init := ()) fun ci i _ => do
+        let .ofTacticInfo tac := i | return
+        unless tac.stx.isOfKind ``Lean.Parser.Tactic.show do return
+        let some _ := tac.stx.getRange? true | return
+        let (goal :: goals) := tac.goalsBefore | return
+        let (goal' :: goals') := tac.goalsAfter | return
+        if goals != goals' then return -- `show` didn't act on first goal -> can't replace with `change`
+        if goal == goal' then return -- same goal, no need to check
+        let diff ← ci.runCoreM do
+          let before ← (do instantiateMVars (← goal.getType)).run' {} { mctx := tac.mctxBefore }
+          let after ← (do instantiateMVars (← goal'.getType)).run' {} { mctx := tac.mctxAfter }
+          return before != after
+        if diff then
+          logLint linter.style.show tac.stx m!"\
+          The `show` tactic should only be used to indicate intermediate goal states for \
+          readability.\nHowever, this tactic invocation changed the goal. Please use `change` \
+          instead for these purposes."
+
+initialize addLinter showLinter
+
+end Style.show
+
 end Mathlib.Linter
diff --git a/Mathlib/Tactic/Linter/UnusedTacticExtension.lean b/Mathlib/Tactic/Linter/UnusedTacticExtension.lean
index 7487d2aab8c..d1688ce8ca2 100644
--- a/Mathlib/Tactic/Linter/UnusedTacticExtension.lean
+++ b/Mathlib/Tactic/Linter/UnusedTacticExtension.lean
@@ -53,6 +53,7 @@ initialize allowedRef : IO.Ref (Std.HashSet SyntaxNodeKind) ←
     `by,
     `null,
     `«]»,
+    `Lean.Parser.Tactic.show,
     -- the following `SyntaxNodeKind`s play a role in silencing `test`s
     `Mathlib.Tactic.successIfFailWithMsg,
     `Mathlib.Tactic.failIfNoProgress,
diff --git a/MathlibTest/ExtractGoal.lean b/MathlibTest/ExtractGoal.lean
index 6c88cad3d6b..b92766ae4bb 100644
--- a/MathlibTest/ExtractGoal.lean
+++ b/MathlibTest/ExtractGoal.lean
@@ -167,9 +167,6 @@ example : ∀ n, n < n + 1 := by
 info: theorem _example.extracted_1 (m : ℕ) (this : m < m.succ.succ) : m < m + 1 := sorry
 ---
 warning: declaration uses 'sorry'
----
-warning: 'show _' tactic does nothing
-note: this linter can be disabled with `set_option linter.unusedTactic false`
 -/
 #guard_msgs in
 example : ∀ n, n < n + 1 := by
diff --git a/MathlibTest/LintStyle.lean b/MathlibTest/LintStyle.lean
index c26c86c1bd8..ca8aba69938 100644
--- a/MathlibTest/LintStyle.lean
+++ b/MathlibTest/LintStyle.lean
@@ -495,3 +495,49 @@ def aux : Nat := 1
 def aux' : Nat := 1

 end openClassical
+
+/- Tests for the `show` linter -/
+section showLinter
+
+set_option linter.style.show true
+
+-- The linter doesn't complain if the goal stays the same
+
+#guard_msgs in
+example : 1 + 2 = 3 := by
+  show 1 + 2 = 3
+  rfl
+
+-- Binder names are ignored
+
+#guard_msgs in
+example : ∀ a : Nat, a = a := by
+  show ∀ b : Nat, b = b
+  intro
+  rfl
+
+-- Goal changes are linted
+
+/--
+warning: The `show` tactic should only be used to indicate intermediate goal states for readability.
+However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
+note: this linter can be disabled with `set_option linter.style.show false`
+-/
+#guard_msgs in
+example : (fun a => a) 1 = 1 := by
+  show 1 = 1
+  rfl
+
+-- Assigning meta-variables in the goal is also linted
+
+/--
+warning: The `show` tactic should only be used to indicate intermediate goal states for readability.
+However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
+note: this linter can be disabled with `set_option linter.style.show false`
+-/
+#guard_msgs in
+example := by
+  show 1 = 1
+  rfl
+
+end showLinter
diff --git a/lean-toolchain b/lean-toolchain
index 93eb2ee78c7..dafec059168 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-17
+leanprover/lean4:nightly-2025-06-18