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 ≫ (F ⊛ G).obj (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)
⊢ (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) =
    (α_ (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:
simp only [whiskerLeft_id, Category.comp_id, Category.assoc] 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 :
  (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)
⊢ (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) =
    (α_ (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