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 :
  (𝟙 (F.obj x) ▷ (G.obj y ⊗ H.obj z) ≫ F.obj x ◁ (unit G H).app (y, z)) ≫
      (unit F (G ⊛ H)).app (x, y ⊗ z) ≫
        ((F ⊛ G ⊛ H).descOfIsLeftKanExtension (unit F (G ⊛ H)) ((F ⊛ G) ⊛ H)
              ((F ⊠ G ⊛ H).descOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F) (tensor C ⋙ (F ⊛ G) ⊛ H)
                ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).hom ≫
                  (ConcreteCategory.hom
                        (𝟙
                          (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                            prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ (F ⊛ G) ⊛ H)))
                      ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv
                        ((((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
                            (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) ⋯).hom).app
                      ((F ⊛ G) ⊛ H)))).app
          (x ⊗ y ⊗ z) =
    (α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫
      ((ConcreteCategory.hom
                (𝟙
                  (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                    prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ (F ⊛ G) ⊛ H)))
              ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv
                ((((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
                    (tensor C ⋙ (F ⊛ G) ⊛ H))
                  ((corepresentableBy (F ⊛ G) H).homEquiv (𝟙 ((F ⊛ G) ⊛ H)))))).app
          (x, y, z) ≫
        ((F ⊛ G) ⊛ H).map (α_ x y z).hom
⊢ F.obj x ◁ (unit G H).app (y, z) ≫
      (unit F (G ⊛ H)).app (x, y ⊗ z) ≫
        ((F ⊛ G ⊛ H).descOfIsLeftKanExtension (unit F (G ⊛ H)) ((F ⊛ G) ⊛ H)
              ((F ⊠ G ⊛ H).descOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F) (tensor C ⋙ (F ⊛ G) ⊛ H)
                ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).hom ≫
                  (ConcreteCategory.hom
                        (𝟙
                          (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                            prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ (F ⊛ G) ⊛ H)))
                      ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv
                        ((((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
                            (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) ⋯).hom).app
                      ((F ⊛ G) ⊛ H)))).app
          (x ⊗ y ⊗ z) =
    (α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫
      (unit F G).app (x, y) ▷ H.obj z ≫ (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ ((F ⊛ G) ⊛ H).map (α_ x y z).hom

Tactic:
simp only [whiskerRight_tensor, id_whiskerRight, Category.id_comp, Iso.inv_hom_id] at this

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 :
  F.obj x ◁ (unit G H).app (y, z) ≫
      (unit F (G ⊛ H)).app (x, y ⊗ z) ≫
        ((F ⊛ G ⊛ H).descOfIsLeftKanExtension (unit F (G ⊛ H)) ((F ⊛ G) ⊛ H)
              ((F ⊠ G ⊛ H).descOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F) (tensor C ⋙ (F ⊛ G) ⊛ H)
                ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).hom ≫
                  (ConcreteCategory.hom
                        (𝟙
                          (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                            prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ (F ⊛ G) ⊛ H)))
                      ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv
                        ((((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
                            (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) ⋯).hom).app
                      ((F ⊛ G) ⊛ H)))).app
          (x ⊗ y ⊗ z) =
    (α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫
      ((ConcreteCategory.hom
                (𝟙
                  (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                    prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ (F ⊛ G) ⊛ H)))
              ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv
                ((((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
                    (tensor C ⋙ (F ⊛ G) ⊛ H))
                  ((corepresentableBy (F ⊛ G) H).homEquiv (𝟙 ((F ⊛ G) ⊛ H)))))).app
          (x, y, z) ≫
        ((F ⊛ G) ⊛ H).map (α_ x y z).hom
⊢ F.obj x ◁ (unit G H).app (y, z) ≫
      (unit F (G ⊛ H)).app (x, y ⊗ z) ≫
        ((F ⊛ G ⊛ H).descOfIsLeftKanExtension (unit F (G ⊛ H)) ((F ⊛ G) ⊛ H)
              ((F ⊠ G ⊛ H).descOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F) (tensor C ⋙ (F ⊛ G) ⊛ H)
                ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).hom ≫
                  (ConcreteCategory.hom
                        (𝟙
                          (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                            prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ (F ⊛ G) ⊛ H)))
                      ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv
                        ((((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
                            (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) ⋯).hom).app
                      ((F ⊛ G) ⊛ H)))).app
          (x ⊗ y ⊗ z) =
    (α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫
      (unit F G).app (x, y) ▷ H.obj z ≫ (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ ((F ⊛ G) ⊛ H).map (α_ x y z).hom