simps generates invalid simp lemma

Stream: mathlib4

[Adam Topaz]

In the porting PR !4#2466 it seems that simps is generating some invalid simp lemma on line 266. The error is

Invalid simp lemma CategoryTheory.monoidalCounit_app.
The given definition is not a constructor application:
  (asEquivalence F.toLaxMonoidalFunctor.toFunctor).counitIso.1

I'd like to get this PR moving quickly because there are now multiple porting PRs depending on it (sorry for slacking with this PR!).

I haven't spent much time investigating, but I thought I would mention it here in case someone (@Floris van Doorn ?) knows of a quick fix.

[Adam Topaz]

Here's a cut down version of the decl in question with the relevant data:

@[simps!] -- error here...
def monoidalCounit (F : MonoidalFunctor C D) [IsEquivalence F.toFunctor] :
    (monoidalInverse F).toLaxMonoidalFunctor ⊗⋙ F.toLaxMonoidalFunctor ⟶ LaxMonoidalFunctor.id D :=
  { toNatTrans := F.toFunctor.asEquivalence.counit
    unit := sorry
    tensor := sorry }

[Adam Topaz]

well, it seems that in mathlib3 the only lemma that was generated by simps was docs#category_theory.monoidal_counit_trans_to_nat_trans and for some reason simps! in mathlib4 is trying to go via a counitIso.1 = counitIso.hom. I can fix this by replacing simps! with simps! toNatTrans for now. But this is something that should still be investigated.

[Floris van Doorn]

The default behavior of @[simps] has changed between Lean 3 and Lean 4 when generating simp lemmas for structures extending other structures. The new default is that simps generates all the nested projections, which in this case would be the app field of NatTrans. This is the desired behavior in the algebraic hierarchy.
In the category library this is not always desired (maybe never even), and you want to actually generate the toNatTrans field. You can getsimps to use the previous behavior if you write (untested):

initialize_simps_projections MonoidalNatTrans (-app, +toNatTrans)

You have to do this for every structure in the category theory library that extends another structure.

[Adam Topaz]

Thanks for the clarification Floris! I wonder if errors such as this could be handled more gracefully by progressively dropping the last projection until the error goes away? In this case simps! did indeed just fail with the error above.

[Adam Topaz]

Although such a feature would probably make things harder to diagnose when they go wrong.