From ce1ff03af049c2eeea0fd33adcb6143dedaf6220 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 11 Jan 2025 21:30:41 -0800
Subject: [PATCH] fix: `checkParents` in `grind` (#6611)

This PR fixes one of the sanity check tests used in `grind`.
---
 src/Lean/Meta/Tactic/Grind/Inv.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Inv.lean b/src/Lean/Meta/Tactic/Grind/Inv.lean
index 0b374a441f..aab448815f 100644
--- a/src/Lean/Meta/Tactic/Grind/Inv.lean
+++ b/src/Lean/Meta/Tactic/Grind/Inv.lean
@@ -58,9 +58,12 @@ private def checkParents (e : Expr) : GoalM Unit := do
           found := true
           break
       -- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`.
-      if let .forallE _ d _ _ := parent then
+      if let .forallE _ d b _ := parent then
         if (← checkChild d) then
           found := true
+        unless b.hasLooseBVars do
+          if (← checkChild b) then
+            found := true
       unless found do
         assert! (← checkChild parent.getAppFn)
   else