Tip on shortening code

Stream: mathlib4

[Nicolas Rolland]

Is there any trick to avoid writing this long mess of isos that is plug below ?

import Mathlib.CategoryTheory.Monoidal.Types.Basic
import Mathlib.CategoryTheory.Products.Associator
import Mathlib.CategoryTheory.Products.Basic

namespace CategoryTheory

variable (A B C D : Type*) [Category A] [Category B] [Category C] [Category D]

abbrev Dist := Dᵒᵖ × C ⥤ Type

def times (P : Dist A B) (Q: Dist C D) :  Dist (A × C) (B × D) :=
  let plug  : (B × D)ᵒᵖ  × (A × C) ⥤ (Bᵒᵖ × A) × Dᵒᵖ × C  :=
    Functor.prod ((prodOpEquiv B).functor) (𝟭 _) ⋙ prod.associator _ _ _ ⋙
    Functor.prod (𝟭 _)  (prod.inverseAssociator  _ _ _ ) ⋙
    Functor.prod (𝟭 _) (Functor.prod (Prod.swap _ _) (𝟭 _) ) ⋙
     Functor.prod (𝟭 _) (prod.associator _ _ _) ⋙
    (prod.inverseAssociator  _ _ _ )
  plug ⋙ Functor.prod P Q ⋙ MonoidalCategory.tensor Type

end CategoryTheory

Hopefully by coherence might help with some parts once I have #15258 in (which gives a monoidal instance for Cat)

[Floris van Doorn]

You can teach calc to write compositions of functors and gcongr to apply Functor.prod (assuming that gcongr is willing to produce data, not just proofs). That will not make your definition shorter, but almost certainly more readable.