fix: unexpected kernel projection issue in grind

This PR fixes the unexpected kernel projection issue reported by

closes #9187

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

@@ -378,7 +378,7 @@ where
       reportIssue! "unexpected metadata found during internalization{indentExpr e}\n`grind` uses a pre-processing step that eliminates metadata"
       mkENode' e generation
     | .proj .. =>
-      reportIssue! "unexpected kernel projection term during internalization{indentExpr e}\n`grind` uses a pre-processing step that folds them as projection applications, the pre-processor should have failed to fold this term"
+      reportIssue! "unexpected kernel projection term during internalization{indentExpr e}\n`grind` uses a pre-processing step that folds them as projection applications, the pre-processor failed to fold this term"
       mkENode' e generation
     | .app .. =>
       if (← isLitValue e) then

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

@@ -84,7 +84,7 @@ def mkChoice (proof : Expr) (subgoals : List Goal) (generation : Nat) : SearchM
 /--
 Create an auxiliary metavariable with the same type and tag of the metavariable
 associated with the current goal.
-We use this function to perform `cases` on the current goal without eagerly assignining it.
+We use this function to perform `cases` on the current goal without eagerly assigning it.
 -/
 def mkAuxMVarForCurrGoal : SearchM MVarId := withCurrGoalContext do
   let mvarId := (← getGoal).mvarId

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

@@ -144,8 +144,10 @@ def foldProjs (e : Expr) : MetaM Expr := do
         F ⟶ G
       ```
       We should make `mkProjection` more robust.
+
+      The `mkProjection` function may create new kernel projections. So, we must use `.visit`.
       -/
-      return .done (← withDefault <| mkProjection s fieldName)
+      return .visit (← withDefault <| mkProjection s fieldName)
     else
       trace[grind.issues] "found `Expr.proj` with invalid field index `{idx}`{indentExpr e}"
       return .done e

tests/lean/run/grind_issue_9187.lean

@@ -0,0 +1,23 @@
+structure Cat (C : Type) where
+  hom : C → C → Type
+  comp {x y z : C} (f : hom x y) (g : hom y z) : hom x z
+  id x : hom x x
+
+structure Foo {C D : Type} (ℭ₁ : Cat C) (ℭ₂ : Cat D) where
+  obj : C → D
+
+variable {C D : Type} {ℭ₁ : Cat C} {ℭ₂ : Cat D}
+
+structure Iso (x y : C) where
+  hom : ℭ₁.hom x y
+  inv : ℭ₁.hom y x
+  hom_inv_id : ℭ₁.comp hom inv = ℭ₁.id _
+  inv_hom_id : ℭ₁.comp hom inv = ℭ₁.id _
+
+attribute [grind =] Iso.hom_inv_id Iso.inv_hom_id
+
+#guard_msgs in -- Should not produce any issues
+set_option trace.grind.issues true in
+example (F G : Foo ℭ₁ ℭ₂) (e : ∀ (x : C), Iso (F.obj x) (G.obj x)) (x : C) :
+    ℭ₂.comp (e x).hom (e x).inv = ℭ₂.id _ := by
+  grind