From 4d9129d5f1836b424b0fa4dadd1f56118b4641e7 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Sat, 11 Jul 2026 10:41:10 -0400
Subject: [PATCH] fix(GRewrite): preserve binder names in a forall

---
 Mathlib/Tactic/GRewrite/Core.lean |  5 ++++-
 MathlibTest/Tactic/GRewrite.lean  | 11 +++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/GRewrite/Core.lean b/Mathlib/Tactic/GRewrite/Core.lean
index db0ff04ad806a9..2fa23ad68cea53 100644
--- a/Mathlib/Tactic/GRewrite/Core.lean
+++ b/Mathlib/Tactic/GRewrite/Core.lean
@@ -323,7 +323,10 @@ partial def grewriteCore (relName : Name) (rel? : Option Expr) (e : Expr) (forwa
     for gcongrLem in lemmas do
       if gcongrLem.forGrw then
         if ← processGCongrLemma goal.mvarId! gcongrLem forward config then
-          return (← instantiateMVars mvar, goal)
+          -- Preserve the binder name/info in a forall.
+          match e, ← instantiateMVars mvar with
+          | .forallE n _ _ bi, .forallE _ d b _ => return some (.forallE n d b bi, goal)
+          | _, result => return some (result, goal)
         setMCtx mctx
   -- Cache the fact that there was nothing to rewrite.
   modify fun s ↦ { s with cache := s.cache.insert cacheKey }
diff --git a/MathlibTest/Tactic/GRewrite.lean b/MathlibTest/Tactic/GRewrite.lean
index 972184032da8e4..b8daa55698702d 100644
--- a/MathlibTest/Tactic/GRewrite.lean
+++ b/MathlibTest/Tactic/GRewrite.lean
@@ -129,6 +129,17 @@ example {a b : Nat} (h : a < b) (f : Nat → Nat) (hf : ∀ i, 0 ≤ f i) :
   trace_state
   rfl
 
+/--
+trace: α : Type ?u.3
+X Y Z W : Set α
+⊢ ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), max a b ≤ max a b
+-/
+#guard_msgs in
+example : ∀ {α : Type*} [LinearOrder α] (a b : α), min a b ≤ max a b := by
+  grw [@inf_le_sup]
+  trace_state
+  intros; rfl
+
 end subsets
 
 section rationals