diff --git a/LeanPool/RootSystem/An.lean b/LeanPool/RootSystem/An.lean
index 10d4b20f26..62ab7191d2 100644
--- a/LeanPool/RootSystem/An.lean
+++ b/LeanPool/RootSystem/An.lean
@@ -236,8 +236,11 @@ theorem pairing_formula {n : ℕ} [NeZero n] (J K : SignedInterval n) :
       aesop;
     · lia;
   rw [← Finset.mul_sum _ _ _]
+  -- Package the bounds separately to preserve the existing generated proof declarations.
+  let intervalBounds : J.i ≤ J.j ∧ K.i ≤ K.j := by
+    as_aux_lemma => exact ⟨J.hij, K.hij⟩
   simp_all +decide [Finset.sum_add_distrib, Finset.sum_sub_distrib]
-  grind +suggestions
+  grind only [Fin.le_def, Fin.lt_def]
 
 theorem pairing_self {n : ℕ} [NeZero n] (J : SignedInterval n) :
     (ZnPairing n (α J)) (αDual J) = 2 := by