fix: missing case in checkParents

This PR fixes a bug in the sanity checkers for the `grind` tactic.

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Inv.lean

@@ -57,6 +57,10 @@ private def checkParents (e : Expr) : GoalM Unit := do
         if (← checkChild arg) then
           found := true
           break
+      -- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`.
+      if let .forallE _ d _ _ := parent then
+        if (← checkChild d) then
+          found := true
       unless found do
         assert! (← checkChild parent.getAppFn)
   else

tests/lean/run/grind_ematch2.lean

@@ -0,0 +1,19 @@
+grind_pattern Array.size_set => Array.set a i v h
+grind_pattern Array.get_set_eq  => a.set i v h
+grind_pattern Array.get_set_ne => (a.set i v hi)[j]
+
+set_option grind.debug true
+set_option trace.grind.ematch.pattern true
+set_option trace.grind.ematch.instance true
+
+example (as bs cs : Array α) (v₁ v₂ : α)
+        (i₁ i₂ j : Nat)
+        (h₁ : i₁ < as.size)
+        (h₂ : bs = as.set i₁ v₁)
+        (h₃ : i₂ < bs.size)
+        (h₃ : cs = bs.set i₂ v₂)
+        (h₄ : i₁ ≠ j ∧ i₂ ≠ j)
+        (h₅ : j < cs.size)
+        (h₆ : j < as.size)
+        : cs[j] = as[j] := by
+  grind