diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index bc320bda42..956c7e622e 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -425,7 +425,13 @@ Sets symbol priorities for the E-matching pattern inference procedure used in `g
 -/
 
 -- The following symbols are never used in E-matching patterns
-attribute [grind symbol 0] Eq HEq Iff And Or Not
+attribute [grind symbol 0] Eq HEq Iff And Or Not ite dite
+/-
+Remark for `ite` and `dite`: recall the then/else branches
+are only internalized after `grind` decided whether the condition is
+`True`/`False`. Thus, they **must** not be used a `grind` patterns.
+-/
+
 -- The following symbols are only used as the root pattern symbol if there isn't another option
 attribute [grind symbol low] HAdd.hAdd HSub.hSub HMul.hMul Dvd.dvd HDiv.hDiv HMod.hMod
 
diff --git a/tests/lean/run/grind_9572.lean b/tests/lean/run/grind_9572.lean
new file mode 100644
index 0000000000..c6da2b815c
--- /dev/null
+++ b/tests/lean/run/grind_9572.lean
@@ -0,0 +1,41 @@
+def List.Disjoint (l₁ l₂ : List α) : Prop :=
+  ∀ ⦃a⦄, a ∈ l₁ → a ∈ l₂ → False
+
+
+/--
+error: `grind` failed
+case grind
+i n : Nat
+f : Nat → List (List Nat)
+l : List Nat
+h :
+  ¬List.Pairwise
+      (fun x y =>
+        (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+          (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
+      l
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] ¬List.Pairwise
+            (fun x y =>
+              (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+                (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
+            l
+  [eqc] False propositions
+    [prop] List.Pairwise
+          (fun x y =>
+            (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+              (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
+          l
+-/
+#guard_msgs in
+theorem test (f : Nat → List (List Nat)) {l : List Nat} :
+    l.Pairwise
+      (fun x y ↦
+        (if x ^ i ≤ n then List.map (fun m ↦ x :: m) (f x) else []).Disjoint
+        (if y ^ i ≤ n then List.map (fun m ↦ y :: m) (f y) else [])) := by
+  -- TODO: fix patterns in standard library
+  -- We had to disable `List.pairwise_iff_forall_sublist` otherwise an unbounded
+  -- number of instances is produced.
+  grind [-List.pairwise_iff_forall_sublist]