grind on `CostructuredArrow.w`

Stream: mathlib4

[Robin Carlier]

I was experimenting with grind and was very surprised to see the result of annotating docs#CategoryTheory.CostructuredArrow.w with grind.

as a reminder, the lemma has type

∀ {C : Type u₁} [inst : Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : Category.{v₂, u₂} D] {T : D} {S : C ⥤ D}
  {A B : CostructuredArrow S T} (f : A ⟶ B), S.map f.left ≫ B.hom = A.hom

and the generated pattern is

/--
info: w: [@CategoryStruct.comp #6 _ (@Functor.obj #8 #7 _ #5 #3 (@Comma.left _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #2)) (@Functor.obj _ _ _ _ #3 (@Comma.left _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #1)) (@Functor.obj `[Discrete
    PUnit.{1}] `[discreteCategory
    PUnit.{1}] _ _ (@Functor.obj _ _ (Functor `[Discrete
      PUnit.{1}] `[discreteCategory
      PUnit.{1}] _ _) _ (Functor.const `[Discrete
      PUnit.{1}] `[discreteCategory
      PUnit.{1}] _ _) #4) (@Comma.right _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #1)) (@Functor.map _ _ _ _ #3 (@Comma.left _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #2) (@Comma.left _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #1) (@CommaMorphism.left _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #2 #1 #0)) (@Comma.hom _ _ `[Discrete
    PUnit.{1}] `[discreteCategory
    PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
      PUnit.{1}] `[discreteCategory
      PUnit.{1}] _ _) _ (Functor.const `[Discrete PUnit.{1}] `[discreteCategory PUnit.{1}] _ _) #4) #1)]
-/
#guard_msgs in
attribute [grind?] _root_.CategoryTheory.CostructuredArrow.w

which looks like a problem for making it trigger in nice situations

I suspect grind is trying to unfold the definitions for CostructuredArrows and their morphisms (which under the hood are morphisms in Comma categories with functors involving Discrete PUnit), where it clearly shouldn’t (perhaps because calling left and hom on objects leave no choice but to infer them as objects /homs in commas, and the underlying problem is in fact that we abuse the defeq between CostructuredArrows and Commas?). @Kim Morrison do you have an idea of the culprit/know how to fix this?