Simp and nested application of functors to isomorphisms

Stream: mathlib4

[Robin Carlier]

import Mathlib.CategoryTheory.Iso

open CategoryTheory

variable (C D E : Type*) [Category C] [Category D] [Category E]

lemma easy {X Y : C} (e : X ≅ Y) (F : C ⥤ D) :
    F.map (e.hom) ≫ F.map (e.inv) = 𝟙 _ := by
  simp -- works

lemma less_easy {X Y : C} (e : X ≅ Y) (F : C ⥤ D) (G : D ⥤ E) :
    G.map (F.map (e.hom)) ≫ G.map (F.map (e.inv)) = 𝟙 _ := by
  simp -- fails; simp [← G.map_comp] works.

Here, the fix is easy and simp [← Functor.map_comp] does the job, but in more complex proofs, it sometimes happens that a simp call get "stuck" on expressions like this, so has to be turned to a big simp only call, followed by a regular simp call.

In CategoryTheory/NatIso.lean, it seems a similar problem is taken care of by having simp lemmas for some nested expressions, e.g docs#CategoryTheory.Iso.inv_hom_id_app_app_app. Should we add similar simp lemmas stating F₁.map (F₂.map ⋯ Fₙ.map (e.hom)) ≫ F₁.map (F₂.map ⋯ Fₙ.map (e.inv)) = 𝟙 _ up to a reasonable n (e.g n = 5)? This is a bit ugly and I wonder if there is a better way to do such things.

[Joël Riou]

We could certainly add a few more of such lemmas like Functor.map_map_hom_inv_id, but I would say only if it improves automation significantly for specific new additions to the library. I added Iso.inv_hom_id_app_app_app specifically in order to deal with functors in three variables, and hopefully, we should not need more...

[Kevin Buzzard]

Can this be done with a simproc?

[Kim Morrison]

I would suggest just waiting for the arrival of grind. My experiments so far with the category theory library suggest that it works very well in situations like this.

[Robin Carlier]

I did not have the patience to wait for grind, and in #PR reviews > #24452 + #24454: `rotate_isos` tactic I propose a tactic that can in particular generate "on the fly" such lemmas.

[Robin Carlier]

I found myself very annoyed by this again (in the context rather big computations with bicategories, where I would end up with terms of the form `A ◁ B ◁ C ◁ D ◁ e.inv ▷ E ▷ F ▷ G ▷ H ≫ A ◁ B ◁ C ◁ D ◁ e.hom ▷ E ▷ F ▷ G ▷ H that wouldn’t simplify without doing some backwards rewriting dance.)

So as Kevin suggested, I figured that might be a job for a simproc (and also an occasion for me to learn a few things), and I wrote #33822. Compared to my last attempt in the post above (which tried to do things in a very brute-forcy and ad hoc way), this time my attempt uses the @[push] attribute and the push tactic/simproc behind the curtains, so the simproc capabilities to "understand" new instances of this patterns are easily extended simply by registering the right IsIso instances and tagging the right lemmas with @[push] (unsurprisingly, it suffices to tag the lemmas that "push" the inverses inwards, this is somewhat opposite to the simp normal forms in the library, which tend to "pull" inverses outwards e.g docs#CategoryTheory.Functor.map_inv).

[Jovan Gerbscheid]

Are you planning to also add the rotate_isos tactic/simproc after #33822 is merged, or does the cancelIso simproc suffice?

[Robin Carlier]

Yes, I am planning to revive rotate_isos as well (it is still wip right now), as the main use case for rotate_isos was the elaborator rotate_isos% that generates rotated versions of lemmas on the fly, which can’t really be handled by cancelIso alone. The implementation would be using cancelIso under the hood.