From ec80de231eb1d3d726ff7f390a293ccd81ab7886 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 24 Dec 2024 23:45:18 +0100
Subject: [PATCH] fix: `checkParents` in `grind` (#6442)

This PR fixes the `checkParents` sanity check in `grind`.
---
 src/Lean/Meta/Tactic/Grind/Inv.lean             | 7 ++++---
 tests/lean/run/grind_propagate_connectives.lean | 4 ++++
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Inv.lean b/src/Lean/Meta/Tactic/Grind/Inv.lean
index 7d4e39927a..c30a425e27 100644
--- a/src/Lean/Meta/Tactic/Grind/Inv.lean
+++ b/src/Lean/Meta/Tactic/Grind/Inv.lean
@@ -40,9 +40,10 @@ private def checkParents (e : Expr) : GoalM Unit := do
       let mut found := false
       -- There is an argument `arg` s.t. root of `arg` is `e`.
       for arg in parent.getAppArgs do
-        if isSameExpr (← getRoot arg) e then
-          found := true
-          break
+        if let some argRoot ← getRoot? arg then
+          if isSameExpr argRoot e then
+            found := true
+            break
       assert! found
   else
     -- All the parents are stored in the root of the equivalence class.
diff --git a/tests/lean/run/grind_propagate_connectives.lean b/tests/lean/run/grind_propagate_connectives.lean
index 3f343a1ca4..8a71d40ae7 100644
--- a/tests/lean/run/grind_propagate_connectives.lean
+++ b/tests/lean/run/grind_propagate_connectives.lean
@@ -59,3 +59,7 @@ warning: declaration uses 'sorry'
 example : ((p₁ ∧ p₂) ∨ q ∨ r) → ((p₂ ∧ p₁) ∨ ¬q) → p₂ = False → False := by
   grind_test
   sorry
+
+example (p q r : Prop) : p ∨ (q ↔ r) → p = False → False := by
+  grind_test
+  sorry