fix: checkParents in grind (#6442)

This PR fixes the `checkParents` sanity check in `grind`.

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.

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