Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
F G : C ⥤ V
inst✝⁵ : DayConvolution F G
H : C ⥤ V
inst✝⁴ : DayConvolution G H
inst✝³ : DayConvolution F (G ⊛ H)
inst✝² : DayConvolution (F ⊛ G) H
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
x y z : C
this :
  (unit F G).app (x, y) ▷ H.obj z ≫
      (unit (F ⊛ G) H).app (x ⊗ y, z) ≫
        (((F ⊛ G) ⊛ H).descOfIsLeftKanExtension (unit (F ⊛ G) H) (F ⊛ G ⊛ H)
              (((F ⊛ G) ⊠ H).descOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H) (tensor C ⋙ F ⊛ G ⊛ H)
                ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
                  ((ConcreteCategory.hom
                      (𝟙
                        (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                          prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ F ⊛ G ⊛ H)))
                    ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).inv ≫
                      ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
                            (tensor C ⋙ F ⊛ G ⊛ H))
                          ((corepresentableBy F (G ⊛ H)).homEquiv (𝟙 (F ⊛ G ⊛ H))) ≫
                        ((whiskeringLeft (C × C × C) C V).map
                              (NatIso.ofComponents (fun x ↦ α_ x.1 x.2.1 x.2.2) ⋯).inv).app
                          (F ⊛ G ⊛ H)))))).app
          ((x ⊗ y) ⊗ z) =
    ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
          ((ConcreteCategory.hom
              (𝟙
                (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                  prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ F ⊛ G ⊛ H)))
            ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).inv ≫
              ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
                    (tensor C ⋙ F ⊛ G ⊛ H))
                  ((corepresentableBy F (G ⊛ H)).homEquiv (𝟙 (F ⊛ G ⊛ H))) ≫
                ((whiskeringLeft (C × C × C) C V).map (NatIso.ofComponents (fun x ↦ α_ x.1 x.2.1 x.2.2) ⋯).inv).app
                  (F ⊛ G ⊛ H)))).app
      ((x, y), z)
⊢ ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
          ((ConcreteCategory.hom
              (𝟙
                (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                  prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ F ⊛ G ⊛ H)))
            ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).inv ≫
              ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
                    (tensor C ⋙ F ⊛ G ⊛ H))
                  ((corepresentableBy F (G ⊛ H)).homEquiv (𝟙 (F ⊛ G ⊛ H))) ≫
                ((whiskeringLeft (C × C × C) C V).map (NatIso.ofComponents (fun x ↦ α_ x.1 x.2.1 x.2.2) ⋯).inv).app
                  (F ⊛ G ⊛ H)))).app
      ((x, y), z) =
    (α_ (F.obj x) (G.obj y) (H.obj z)).hom ≫
      F.obj x ◁ (unit G H).app (y, z) ≫ (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ (F ⊛ G ⊛ H).map (α_ x y z).inv

Tactic:
dsimp [Functor.FullyFaithful.homEquiv, Equivalence.fullyFaithfulFunctor, prod.associativity]

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
F G : C ⥤ V
inst✝⁵ : DayConvolution F G
H : C ⥤ V
inst✝⁴ : DayConvolution G H
inst✝³ : DayConvolution F (G ⊛ H)
inst✝² : DayConvolution (F ⊛ G) H
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
x y z : C
this :
  (unit F G).app (x, y) ▷ H.obj z ≫
      (unit (F ⊛ G) H).app (x ⊗ y, z) ≫
        (((F ⊛ G) ⊛ H).descOfIsLeftKanExtension (unit (F ⊛ G) H) (F ⊛ G ⊛ H)
              (((F ⊛ G) ⊠ H).descOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H) (tensor C ⋙ F ⊛ G ⊛ H)
                ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
                  ((ConcreteCategory.hom
                      (𝟙
                        (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                          prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ F ⊛ G ⊛ H)))
                    ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).inv ≫
                      ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
                            (tensor C ⋙ F ⊛ G ⊛ H))
                          ((corepresentableBy F (G ⊛ H)).homEquiv (𝟙 (F ⊛ G ⊛ H))) ≫
                        ((whiskeringLeft (C × C × C) C V).map
                              (NatIso.ofComponents (fun x ↦ α_ x.1 x.2.1 x.2.2) ⋯).inv).app
                          (F ⊛ G ⊛ H)))))).app
          ((x ⊗ y) ⊗ z) =
    ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
          ((ConcreteCategory.hom
              (𝟙
                (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                  prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ F ⊛ G ⊛ H)))
            ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).inv ≫
              ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
                    (tensor C ⋙ F ⊛ G ⊛ H))
                  ((corepresentableBy F (G ⊛ H)).homEquiv (𝟙 (F ⊛ G ⊛ H))) ≫
                ((whiskeringLeft (C × C × C) C V).map (NatIso.ofComponents (fun x ↦ α_ x.1 x.2.1 x.2.2) ⋯).inv).app
                  (F ⊛ G ⊛ H)))).app
      ((x, y), z)
⊢ ({ functor := prod.associator C C C, inverse := prod.inverseAssociator C C C, unitIso := Iso.refl (𝟭 ((C × C) × C)),
                  counitIso := Iso.refl (prod.inverseAssociator C C C ⋙ prod.associator C C C),
                  functor_unitIso_comp := ⋯ }.funInvIdAssoc
              ((F ⊠ G) ⊠ H)).inv.app
        ((x, y), z) ≫
      ((ConcreteCategory.hom
                (𝟙
                  (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                    prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ F ⊛ G ⊛ H)))
              ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).inv ≫
                ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
                      (tensor C ⋙ F ⊛ G ⊛ H))
                    ((corepresentableBy F (G ⊛ H)).homEquiv (𝟙 (F ⊛ G ⊛ H))) ≫
                  ((whiskeringLeft (C × C × C) C V).map (NatIso.ofComponents (fun x ↦ α_ x.1 x.2.1 x.2.2) ⋯).inv).app
                    (F ⊛ G ⊛ H))).app
          (x, y, z) ≫
        ({ functor := prod.associator C C C, inverse := prod.inverseAssociator C C C,
                    unitIso := Iso.refl (𝟭 ((C × C) × C)),
                    counitIso := Iso.refl (prod.inverseAssociator C C C ⋙ prod.associator C C C),
                    functor_unitIso_comp := ⋯ }.funInvIdAssoc
                ((tensor C).prod (𝟭 C) ⋙ tensor C ⋙ F ⊛ G ⊛ H)).hom.app
          ((x, y), z) =
    (α_ (F.obj x) (G.obj y) (H.obj z)).hom ≫
      F.obj x ◁ (unit G H).app (y, z) ≫ (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ (F ⊛ G ⊛ H).map (α_ x y z).inv