fix: change show tactic to work as documented (#7395)

This PR changes the `show t` tactic to match its documentation.
Previously it was a synonym for `change t`, but now it finds the first
goal that unifies with the term `t` and moves it to the front of the
goal list.

src/Init/Control/Lawful/Basic.lean

@@ -148,7 +148,7 @@ attribute [simp] pure_bind bind_assoc bind_pure_comp
 attribute [grind] pure_bind
 
 @[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
-  show x >>= (fun a => pure (id a)) = x
+  change x >>= (fun a => pure (id a)) = x
   rw [bind_pure_comp, id_map]
 
 /--

src/Init/Control/Lawful/Instances.lean

@@ -58,7 +58,7 @@ protected theorem bind_pure_comp [Monad m] (f : α → β) (x : ExceptT ε m α)
   intros; rfl
 
 protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y := by
-  show (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y
+  change (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y
   rw [← ExceptT.bind_pure_comp]
   apply ext
   simp [run_bind]
@@ -70,7 +70,7 @@ protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad
     cases b <;> simp [comp, Except.map, const]
 
 protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = const α id <$> x <*> y := by
-  show (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y
+  change (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y
   rw [← ExceptT.bind_pure_comp]
   apply ext
   simp [run_bind]
@@ -206,15 +206,15 @@ theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f :
     (monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
 
 @[simp] theorem run_seq {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = (f.run s >>= fun fs => (fun (p : α × σ) => (fs.1 p.1, p.2)) <$> x.run fs.2) := by
-  show (f >>= fun g => g <$> x).run s = _
+  change (f >>= fun g => g <$> x).run s = _
   simp
 
 @[simp] theorem run_seqRight [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
-  show (x >>= fun _ => y).run s = _
+  change (x >>= fun _ => y).run s = _
   simp
 
 @[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
-  show (x >>= fun a => y >>= fun _ => pure a).run s = _
+  change (x >>= fun a => y >>= fun _ => pure a).run s = _
   simp
 
 theorem seqRight_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x *> y = const α id <$> x <*> y := by

src/Init/Core.lean

@@ -2252,7 +2252,7 @@ theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
     Quot.liftOn f
       (fun (f : ∀ (x : α), β x) => f x)
       (fun _ _ h => h x)
-  show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
+  change extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
   exact congrArg extfunApp (Quot.sound h)
 
 /--

src/Init/Data/Array/Basic.lean

@@ -246,7 +246,7 @@ def swap (xs : Array α) (i j : @& Nat) (hi : i < xs.size := by get_elem_tactic)
   xs'.set j v₁ (Nat.lt_of_lt_of_eq hj (size_set _).symm)
 
 @[simp] theorem size_swap {xs : Array α} {i j : Nat} {hi hj} : (xs.swap i j hi hj).size = xs.size := by
-  show ((xs.set i xs[j]).set j xs[i]
+  change ((xs.set i xs[j]).set j xs[i]
     (Nat.lt_of_lt_of_eq hj (size_set _).symm)).size = xs.size
   rw [size_set, size_set]
 

src/Init/Data/BitVec/Bitblast.lean

@@ -1023,7 +1023,7 @@ theorem DivModState.toNat_shiftRight_sub_one_eq
     {args : DivModArgs w} {qr : DivModState w} (h : qr.Poised args) :
     args.n.toNat >>> (qr.wn - 1)
     = (args.n.toNat >>> qr.wn) * 2 + (args.n.getLsbD (qr.wn - 1)).toNat := by
-  show BitVec.toNat (args.n >>> (qr.wn - 1)) = _
+  change BitVec.toNat (args.n >>> (qr.wn - 1)) = _
   have {..} := h -- break the structure down for `omega`
   rw [shiftRight_sub_one_eq_shiftConcat args.n h.hwn_lt]
   rw [toNat_shiftConcat_eq_of_lt (k := w - qr.wn)]

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -3,7 +3,6 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro
 -/
-
 module
 
 prelude
@@ -99,7 +98,7 @@ theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := natCast_emod m n
 theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
   | ofNat _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
   | ofNat m, -[n+1] => by
-    show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
+    change (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
     rw [Int.neg_mul_neg]; exact congrArg ofNat <| Nat.mod_add_div ..
   | -[_+1], 0 => by rw [emod_zero]; rfl
   | -[m+1], succ n => aux m n.succ
@@ -149,7 +148,7 @@ theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c
   fun {k n} => @fun
   | ofNat _ => congrArg ofNat <| Nat.add_mul_div_right _ _ k.succ_pos
   | -[m+1] => by
-    show ((n * k.succ : Nat) - m.succ : Int).ediv k.succ = n - (m / k.succ + 1 : Nat)
+    change ((n * k.succ : Nat) - m.succ : Int).ediv k.succ = n - (m / k.succ + 1 : Nat)
     by_cases h : m < n * k.succ
     · rw [← Int.ofNat_sub h, ← Int.ofNat_sub ((Nat.div_lt_iff_lt_mul k.succ_pos).2 h)]
       apply congrArg ofNat
@@ -158,7 +157,7 @@ theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c
       have H {a b : Nat} (h : a ≤ b) : (a : Int) + -((b : Int) + 1) = -[b - a +1] := by
         rw [negSucc_eq, Int.ofNat_sub h]
         simp only [Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, Int.add_left_comm, Int.add_assoc]
-      show ediv (↑(n * succ k) + -((m : Int) + 1)) (succ k) = n + -(↑(m / succ k) + 1 : Int)
+      change ediv (↑(n * succ k) + -((m : Int) + 1)) (succ k) = n + -(↑(m / succ k) + 1 : Int)
       rw [H h, H ((Nat.le_div_iff_mul_le k.succ_pos).2 h)]
       apply congrArg negSucc
       rw [Nat.mul_comm, Nat.sub_mul_div_of_le]; rwa [Nat.mul_comm]

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -3,7 +3,6 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro, Kim Morrison, Markus Himmel
 -/
-
 module
 
 prelude
@@ -332,17 +331,17 @@ theorem fdiv_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.fdiv b = a / b := by
 theorem tmod_add_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
   | ofNat _, ofNat _ => congrArg ofNat (Nat.mod_add_div ..)
   | ofNat m, -[n+1] => by
-    show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
+    change (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
     rw [Int.neg_mul_neg]; exact congrArg ofNat (Nat.mod_add_div ..)
   | -[m+1], 0 => by
-    show -(↑((succ m) % 0) : Int) + 0 * -↑(succ m / 0) = -↑(succ m)
+    change -(↑((succ m) % 0) : Int) + 0 * -↑(succ m / 0) = -↑(succ m)
     rw [Nat.mod_zero, Int.zero_mul, Int.add_zero]
   | -[m+1], ofNat n => by
-    show -(↑((succ m) % n) : Int) + ↑n * -↑(succ m / n) = -↑(succ m)
+    change -(↑((succ m) % n) : Int) + ↑n * -↑(succ m / n) = -↑(succ m)
     rw [Int.mul_neg, ← Int.neg_add]
     exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
   | -[m+1], -[n+1] => by
-    show -(↑(succ m % succ n) : Int) + -↑(succ n) * ↑(succ m / succ n) = -↑(succ m)
+    change -(↑(succ m % succ n) : Int) + -↑(succ n) * ↑(succ m / succ n) = -↑(succ m)
     rw [Int.neg_mul, ← Int.neg_add]
     exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
 
@@ -364,17 +363,17 @@ theorem fmod_add_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
   | 0, ofNat _ | 0, -[_+1] => congrArg ofNat <| by simp
   | succ _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
   | succ m, -[n+1] => by
-    show subNatNat (m % succ n) n + (↑(succ n * (m / succ n)) + n + 1) = (m + 1)
+    change subNatNat (m % succ n) n + (↑(succ n * (m / succ n)) + n + 1) = (m + 1)
     rw [Int.add_comm _ n, ← Int.add_assoc, ← Int.add_assoc,
       Int.subNatNat_eq_coe, Int.sub_add_cancel]
     exact congrArg (ofNat · + 1) <| Nat.mod_add_div ..
   | -[_+1], 0 => by rw [fmod_zero]; rfl
   | -[m+1], succ n => by
-    show subNatNat .. - (↑(succ n * (m / succ n)) + ↑(succ n)) = -↑(succ m)
+    change subNatNat .. - (↑(succ n * (m / succ n)) + ↑(succ n)) = -↑(succ m)
     rw [Int.subNatNat_eq_coe, ← Int.sub_sub, ← Int.neg_sub, Int.sub_sub, Int.sub_sub_self]
     exact congrArg (-ofNat ·) <| Nat.succ_add .. ▸ Nat.mod_add_div .. ▸ rfl
   | -[m+1], -[n+1] => by
-    show -(↑(succ m % succ n) : Int) + -↑(succ n * (succ m / succ n)) = -↑(succ m)
+    change -(↑(succ m % succ n) : Int) + -↑(succ n * (succ m / succ n)) = -↑(succ m)
     rw [← Int.neg_add]; exact congrArg (-ofNat ·) <| Nat.mod_add_div ..
 
 /-- Variant of `fmod_add_fdiv` with the multiplication written the other way around. -/
@@ -575,7 +574,7 @@ theorem neg_one_ediv (b : Int) : -1 / b = -b.sign :=
       · refine Nat.le_trans ?_ (Nat.le_add_right _ _)
         rw [← Nat.mul_div_mul_left _ _ m.succ_pos]
         apply Nat.div_mul_le_self
-      · show m.succ * n.succ ≤ _
+      · change m.succ * n.succ ≤ _
         rw [Nat.mul_left_comm]
         apply Nat.mul_le_mul_left
         apply (Nat.div_lt_iff_lt_mul k.succ_pos).1
@@ -2748,7 +2747,7 @@ theorem bmod_lt {x : Int} {m : Nat} (h : 0 < m) : bmod x m < (m + 1) / 2 := by
   split
   · assumption
   · apply Int.lt_of_lt_of_le
-    · show _ < 0
+    · change _ < 0
       have : x % m < m := emod_lt_of_pos x (natCast_pos.mpr h)
       exact Int.sub_neg_of_lt this
     · exact Int.le.intro_sub _ rfl

src/Init/Data/Int/Lemmas.lean

@@ -339,7 +339,7 @@ protected theorem add_sub_assoc (a b c : Int) : a + b - c = a + (b - c) := by
   match m with
   | 0 => rfl
   | succ m =>
-    show ofNat (n - succ m) = subNatNat n (succ m)
+    change ofNat (n - succ m) = subNatNat n (succ m)
     rw [subNatNat, Nat.sub_eq_zero_of_le h]
 
 @[deprecated negSucc_eq (since := "2025-03-11")]

src/Init/Data/Int/Linear.lean

@@ -1665,7 +1665,7 @@ theorem natCast_sub (x y : Nat)
         (NatCast.natCast x : Int) + -1*NatCast.natCast y
       else
         (0 : Int) := by
-  show (↑(x - y) : Int) = if (↑y : Int) + (-1)*↑x ≤ 0 then ↑x + (-1)*↑y else 0
+  change (↑(x - y) : Int) = if (↑y : Int) + (-1)*↑x ≤ 0 then (↑x : Int) + (-1)*↑y else 0
   rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.one_mul]
   rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.one_mul]
   split

src/Init/Data/List/Pairwise.lean

@@ -159,7 +159,7 @@ theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y →
 
 @[grind =] theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
     Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂)) := by
-  show Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
+  change Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
   rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
   simp only [mem_append, or_comm]
 

src/Init/Data/List/ToArray.lean

@@ -685,7 +685,7 @@ theorem replace_toArray [BEq α] [LawfulBEq α] (l : List α) (a b : α) :
         · rw [if_pos (by omega), if_pos, if_neg]
           · simp only [mem_take_iff_getElem, not_exists]
             intro k hk
-            simpa using h.2 ⟨k, by omega⟩ (by show k < i.1; omega)
+            simpa using h.2 ⟨k, by omega⟩ (by change k < i.1; omega)
           · subst h₃
             simpa using h.1
         · rw [if_neg (by omega)]

src/Init/Data/List/Zip.lean

@@ -312,7 +312,7 @@ theorem map_fst_zip :
   | [], _, _ => rfl
   | _ :: as, _ :: bs, h => by
     simp [Nat.succ_le_succ_iff] at h
-    show _ :: map Prod.fst (zip as bs) = _ :: as
+    change _ :: map Prod.fst (zip as bs) = _ :: as
     rw [map_fst_zip (l₁ := as) h]
   | _ :: _, [], h => by simp at h
 
@@ -324,7 +324,7 @@ theorem map_snd_zip :
   | [], b :: bs, h => by simp at h
   | a :: as, b :: bs, h => by
     simp [Nat.succ_le_succ_iff] at h
-    show _ :: map Prod.snd (zip as bs) = _ :: bs
+    change _ :: map Prod.snd (zip as bs) = _ :: bs
     rw [map_snd_zip (l₂ := bs) h]
 
 theorem map_prod_left_eq_zip {l : List α} {f : α → β} :

src/Init/Data/Nat/Basic.lean

@@ -1069,7 +1069,7 @@ protected theorem sub_lt_sub_right : ∀ {a b c : Nat}, c ≤ a → a < b → a
     exact Nat.sub_lt_sub_right (le_of_succ_le_succ hle) (lt_of_succ_lt_succ h)
 
 protected theorem sub_self_add (n m : Nat) : n - (n + m) = 0 := by
-  show (n + 0) - (n + m) = 0
+  change (n + 0) - (n + m) = 0
   rw [Nat.add_sub_add_left, Nat.zero_sub]
 
 @[simp] protected theorem sub_eq_zero_of_le {n m : Nat} (h : n ≤ m) : n - m = 0 := by

src/Init/Data/Nat/Div/Basic.lean

@@ -76,7 +76,7 @@ private theorem div.go.fuel_congr (x y fuel1 fuel2 : Nat) (hy : 0 < y) (h1 : x <
 termination_by structural fuel1
 
 theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by
-  show Nat.div _ _ = ite _ (Nat.div _ _ + 1) _
+  change Nat.div _ _ = ite _ (Nat.div _ _ + 1) _
   unfold Nat.div
   split
   next =>
@@ -258,7 +258,7 @@ protected def mod : @& Nat → @& Nat → Nat
 instance instMod : Mod Nat := ⟨Nat.mod⟩
 
 protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by
-  show Nat.modCore n m = Nat.mod n m
+  change Nat.modCore n m = Nat.mod n m
   match n, m with
   | 0, _ =>
     rw [Nat.modCore_eq]
@@ -522,7 +522,7 @@ theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - (x + 1)) / n = p -
     rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
     exact Nat.sub_le_sub_left ((div_lt_iff_lt_mul npos).1 (lt_succ_self _)) _
   focus
-    show succ (pred (n * p - x)) ≤ (succ (pred (p - x / n))) * n
+    change succ (pred (n * p - x)) ≤ (succ (pred (p - x / n))) * n
     rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁),
       fun h => succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)] -- TODO: why is the function needed?
     focus

src/Init/Data/Nat/Linear.lean

@@ -149,7 +149,7 @@ instance : LawfulBEq PolyCnstr where
     rw [h₁, h₂, h₃]
   rfl {a} := by
     cases a; rename_i eq lhs rhs
-    show (eq == eq && (lhs == lhs && rhs == rhs)) = true
+    change (eq == eq && (lhs == lhs && rhs == rhs)) = true
     simp
 
 structure ExprCnstr where

src/Init/Data/String/Basic.lean

@@ -586,7 +586,7 @@ decreasing_by
   focus
     rename_i i₀ j₀ _ eq h'
     rw [show (s.next i₀ - sep.next j₀).1 = (i₀ - j₀).1 by
-      show (_ + Char.utf8Size _) - (_ + Char.utf8Size _) = _
+      change (_ + Char.utf8Size _) - (_ + Char.utf8Size _) = _
       rw [(beq_iff_eq ..).1 eq, Nat.add_sub_add_right]; rfl]
     right; exact Nat.sub_lt_sub_left
       (Nat.lt_of_le_of_lt (Nat.le_add_right ..) (Nat.gt_of_not_le (mt decide_eq_true h')))

src/Init/Data/String/Extra.lean

@@ -295,11 +295,11 @@ where
   termination_by text.utf8ByteSize - pos.byteIdx
   decreasing_by
     decreasing_with
-      show text.utf8ByteSize - (text.next (text.next pos)).byteIdx < text.utf8ByteSize - pos.byteIdx
+      change text.utf8ByteSize - (text.next (text.next pos)).byteIdx < text.utf8ByteSize - pos.byteIdx
       have k := Nat.gt_of_not_le <| mt decide_eq_true h
       exact Nat.sub_lt_sub_left k (Nat.lt_trans (String.lt_next text pos) (String.lt_next _ _))
     decreasing_with
-      show text.utf8ByteSize - (text.next pos).byteIdx < text.utf8ByteSize - pos.byteIdx
+      change text.utf8ByteSize - (text.next pos).byteIdx < text.utf8ByteSize - pos.byteIdx
       have k := Nat.gt_of_not_le <| mt decide_eq_true h
       exact Nat.sub_lt_sub_left k (String.lt_next _ _)
 

src/Init/Grind/CommRing/Poly.lean

@@ -206,7 +206,7 @@ instance : LawfulBEq Poly where
     intro a
     induction a <;> simp! [BEq.beq]
     next k m p ih =>
-    show m == m ∧ p == p
+    change m == m ∧ p == p
     simp [ih]
 
 def Poly.denote [CommRing α] (ctx : Context α) (p : Poly) : α :=
@@ -533,7 +533,7 @@ theorem Mon.denote_concat {α} [CommRing α] (ctx : Context α) (m₁ m₂ : Mon
   next p₁ m₁ ih => rw [mul_assoc]
 
 private theorem le_of_blt_false {a b : Nat} : a.blt b = false → b ≤ a := by
-  intro h; apply Nat.le_of_not_gt; show ¬a < b
+  intro h; apply Nat.le_of_not_gt; change ¬a < b
   rw [← Nat.blt_eq, h]; simp
 
 private theorem eq_of_blt_false {a b : Nat} : a.blt b = false → b.blt a = false → a = b := by

src/Init/Internal/Order/Basic.lean

@@ -363,7 +363,7 @@ theorem chain_iterates {f : α → α} (hf : monotone f) : chain (iterates f) :=
       · left; apply hf; assumption
       · right; apply hf; assumption
     case sup c hchain hi ih2 =>
-      show f x ⊑ csup c ∨ csup c ⊑ f x
+      change f x ⊑ csup c ∨ csup c ⊑ f x
       by_cases h : ∃ z, c z ∧ f x ⊑ z
       · left
         obtain ⟨z, hz, hfz⟩ := h
@@ -380,7 +380,7 @@ theorem chain_iterates {f : α → α} (hf : monotone f) : chain (iterates f) :=
         next => contradiction
         next => assumption
   case sup c hchain hi ih =>
-    show rel (csup c) y ∨ rel y (csup c)
+    change rel (csup c) y ∨ rel y (csup c)
     by_cases h : ∃ z, c z ∧ rel y z
     · right
       obtain ⟨z, hz, hfz⟩ := h

src/Init/Meta.lean

@@ -248,7 +248,7 @@ def appendBefore (n : Name) (pre : String) : Name :=
     | num p n => Name.mkNum (Name.mkStr p pre) n
 
 protected theorem beq_iff_eq {m n : Name} : m == n ↔ m = n := by
-  show m.beq n ↔ _
+  change m.beq n ↔ _
   induction m generalizing n <;> cases n <;> simp_all [Name.beq, And.comm]
 
 instance : LawfulBEq Name where

src/Init/Tactics.lean

@@ -535,6 +535,12 @@ syntax (name := change) "change " term (location)? : tactic
 -/
 syntax (name := changeWith) "change " term " with " term (location)? : tactic
 
+/--
+`show t` finds the first goal whose target unifies with `t`. It makes that the main goal,
+performs the unification, and replaces the target with the unified version of `t`.
+-/
+syntax (name := «show») "show " term : tactic
+
 /--
 Extracts `let` and `let_fun` expressions from within the target or a local hypothesis,
 introducing new local definitions.
@@ -864,11 +870,6 @@ The `let` tactic is for adding definitions to the local context of the main goal
   local variables `x : α`, `y : β`, and `z : γ`.
 -/
 macro "let " d:letDecl : tactic => `(tactic| refine_lift let $d:letDecl; ?_)
-/--
-`show t` finds the first goal whose target unifies with `t`. It makes that the main goal,
- performs the unification, and replaces the target with the unified version of `t`.
--/
-macro "show " e:term : tactic => `(tactic| refine_lift show $e from ?_) -- TODO: fix, see comment
 /-- `let rec f : t := e` adds a recursive definition `f` to the current goal.
 The syntax is the same as term-mode `let rec`. -/
 syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic

src/Lean/Elab/Tactic.lean

@@ -50,4 +50,5 @@ import Lean.Elab.Tactic.AsAuxLemma
 import Lean.Elab.Tactic.TreeTacAttr
 import Lean.Elab.Tactic.ExposeNames
 import Lean.Elab.Tactic.SimpArith
+import Lean.Elab.Tactic.Show
 import Lean.Elab.Tactic.Lets

src/Lean/Elab/Tactic/Change.lean

@@ -13,12 +13,18 @@ open Meta
 # Implementation of the `change` tactic
 -/
 
+private def elabChangeDefaultError (p tgt : Expr) : MetaM MessageData := do
+  return m!"\
+    'change' tactic failed, pattern{indentExpr p}\n\
+    is not definitionally equal to target{indentExpr tgt}"
+
 /--
 Elaborates the pattern `p` and ensures that it is defeq to `e`.
 Emulates `(show p from ?m : e)`, returning the type of `?m`, but `e` and `p` do not need to be types.
 Unlike `(show p from ?m : e)`, this can assign synthetic opaque metavariables appearing in `p`.
 -/
-def elabChange (e : Expr) (p : Term) : TacticM Expr := do
+def elabChange (e : Expr) (p : Term) (mkDefeqError : Expr → Expr → MetaM MessageData := elabChangeDefaultError) :
+    TacticM Expr := do
   let p ← runTermElab do
     let p ← Term.elabTermEnsuringType p (← inferType e)
     unless ← isDefEq p e do
@@ -32,10 +38,9 @@ def elabChange (e : Expr) (p : Term) : TacticM Expr := do
     pure p
   withAssignableSyntheticOpaque do
     unless ← isDefEq p e do
-      let (p, tgt) ← addPPExplicitToExposeDiff p e
-      throwError "\
-        'change' tactic failed, pattern{indentExpr p}\n\
-        is not definitionally equal to target{indentExpr tgt}"
+      throwError MessageData.ofLazyM (es := #[p, e]) do
+        let (p, tgt) ← addPPExplicitToExposeDiff p e
+        mkDefeqError p tgt
     instantiateMVars p
 
 /-- `change` can be used to replace the main goal or its hypotheses with

src/Lean/Elab/Tactic/Show.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2025 Robin Arnez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Arnez
+-/
+prelude
+import Lean.Elab.Tactic.Change
+
+namespace Lean.Elab.Tactic
+open Meta
+/-!
+# Implementation of the `show` tactic
+
+The `show p` tactic finds the first goal that `p` unifies with and brings it to the front of the
+goal list. If there were a `first_goal` combinator, it would be like `first_goal change p`.
+-/
+
+def elabShow (newType : Term) : TacticM Unit := do
+  let goals@(goal :: _) ← getGoals | throwNoGoalsToBeSolved
+  go newType goal goals []
+where
+  go (newType : Term) (firstGoal : MVarId) (goals : List MVarId) (prevRev : List MVarId) : TacticM Unit := do
+    match goals with
+    | [] =>
+      -- re-run first goal for error message
+      tryGoal newType firstGoal (← getGoals).tail [] manyError
+    | goal :: goals =>
+      if goals.isEmpty && (prevRev.isEmpty || !(← read).recover) then
+        -- optimization for single goal / last goal without error recovery
+        tryGoal newType goal goals prevRev simpleError
+      else
+        /-
+        Save state manually to make sure that the info state is reverted,
+        since `elabChange` elaborates the pattern each time.
+        -/
+        let state ← saveState
+        Tactic.tryCatch
+          (withoutRecover (tryGoal newType goal goals prevRev simpleError))
+          fun _ => do
+            state.restore true
+            go newType firstGoal goals (goal :: prevRev)
+  tryGoal (newType : Term) (goal : MVarId) (goals : List MVarId) (prevRev : List MVarId) (err : Expr → Expr → MetaM MessageData) : TacticM Unit := do
+    let type ← goal.getType
+    let tag ← goal.getTag
+    goal.withContext do
+      let (tgt', mvars) ← withCollectingNewGoalsFrom
+        (elabChange type newType err)
+        tag `show
+      let goal' ← goal.replaceTargetDefEq tgt'
+      let newGoals := goal' :: prevRev.reverseAux (mvars ++ goals)
+      setGoals newGoals
+  simpleError (p tgt : Expr) : MetaM MessageData := do
+    return m!"\
+      'show' tactic failed, pattern{indentExpr p}\n\
+      is not definitionally equal to target{indentExpr tgt}"
+  manyError (p tgt : Expr) : MetaM MessageData := do
+    return m!"\
+      'show' tactic failed, no goals unify with the given pattern.\n\
+      \n\
+      In the first goal, the pattern{indentExpr p}\n\
+      is not definitionally equal to the target{indentExpr tgt}\n\
+      (Errors for other goals omitted)"
+
+@[builtin_tactic «show»] elab_rules : tactic
+  | `(tactic| show $newType:term) => elabShow newType
+
+end Lean.Elab.Tactic

src/lake/Lake/Util/Name.lean

@@ -56,7 +56,7 @@ theorem eq_anonymous_of_isAnonymous {n : Name} : (h : n.isAnonymous) → n = .an
 
 @[simp] theorem isPrefixOf_append {n m : Name} : ¬ n.hasMacroScopes → ¬ m.hasMacroScopes → n.isPrefixOf (n ++ m) := by
   intro h1 h2
-  show n.isPrefixOf (n.append m)
+  change n.isPrefixOf (n.append m)
   simp_all [Name.append]
   clear h2; induction m <;> simp [*, Name.appendCore, isPrefixOf]
 

tests/lean/interactive/incrementalTactic.lean.expected.out

@@ -61,7 +61,7 @@ s
 { goals := #[{ type := Lean.Widget.TaggedText.tag
                          { subexprPos := "/", diffStatus? := none }
                          (Lean.Widget.TaggedText.text "True"),
-               isInserted? := some false,
+               isInserted? := none,
                isRemoved? := none,
                hyps := #[] }] }
 

tests/lean/run/showTactic.lean

@@ -0,0 +1,160 @@
+/-!
+# Testing the new behavior of the `show` tactic
+
+Implemented in PR #7395.
+-/
+
+/-!
+`show` can change a single goal to a definitionally equivalent one.
+-/
+
+/--
+error: unsolved goals
+x : Nat
+⊢ x - 0 = 3 - 3
+-/
+#guard_msgs in
+example : x = 0 := by
+  show x - 0 = 3 - 3
+
+/-!
+`show` on a single goal fails if the pattern is not defeq to the target.
+-/
+
+/--
+error: 'show' tactic failed, pattern
+  x = 1
+is not definitionally equal to target
+  x = 0
+-/
+#guard_msgs in
+example : x = 0 := by
+  show x = 1
+
+/-!
+`show` on multiple goals picks the first that matches.
+-/
+
+/--
+error: unsolved goals
+case refine_2
+x : Nat
+⊢ x = 1
+
+case refine_1
+x : Nat
+⊢ x = 0
+-/
+#guard_msgs in
+example : x = 0 ∧ x = 1 := by
+  and_intros
+  show _ = 1
+
+/-!
+The matching goal is moved to the front and the order of the others is preserved.
+-/
+
+/--
+error: unsolved goals
+case refine_2.refine_2.refine_1
+x : Nat
+⊢ x = 2
+
+case refine_1
+x : Nat
+⊢ x = 0
+
+case refine_2.refine_1
+x : Nat
+⊢ x = 1
+
+case refine_2.refine_2.refine_2
+x : Nat
+⊢ x = 3
+-/
+#guard_msgs in
+example : x = 0 ∧ x = 1 ∧ x = 2 ∧ x = 3 := by
+  and_intros
+  show _ = 2
+
+/-!
+All goals are first elaborated without error recovery.
+-/
+
+/--
+error: unsolved goals
+case refine_2.refine_2
+a : Unit
+⊢ a = ()
+
+case refine_1
+⊢ () = ()
+
+case refine_2.refine_1
+⊢ () = ()
+-/
+#guard_msgs in
+example : () = () ∧ () = () ∧ (∀ a, a = ()) := by
+  and_intros; all_goals try intro a
+  show a = _
+
+/-!
+The first goal is re-elaborated with error recovery.
+-/
+
+/--
+error: unknown identifier 'a'
+---
+error: unsolved goals
+case refine_1
+⊢ sorry = ()
+
+case refine_2
+⊢ () = ()
+-/
+#guard_msgs in
+example : () = () ∧ () = () := by
+  and_intros
+  show a = _
+
+/-!
+If all unifications fail, the error is from the first goal with a mention that the later goals
+also weren't defeq.
+-/
+
+/--
+error: 'show' tactic failed, no goals unify with the given pattern.
+
+In the first goal, the pattern
+  x = 4
+is not definitionally equal to the target
+  x = 1
+(Errors for other goals omitted)
+-/
+#guard_msgs in
+example : x = 1 ∧ x = 2 ∧ x = 3 := by
+  and_intros
+  show x = 4
+
+/-!
+`show` also works when a mentioned variable only exists in some goals.
+-/
+
+/--
+error: unsolved goals
+case refine_2.refine_2
+c : Nat
+⊢ c = 1
+
+case refine_1
+a : Nat
+⊢ a = 1
+
+case refine_2.refine_1
+b : Nat
+⊢ b = 1
+-/
+#guard_msgs in
+example : (∀ a, a = 1) ∧ (∀ b, b = 1) ∧ (∀ c, c = 1) := by
+  and_intros; all_goals unhygienic intro
+  show c = _