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.