fix(GRewrite): preserve binder names in a forall

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 }

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