Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
z x y : C
⊢ ((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) ≫
        (associator F G H).hom.app ((x ⊗ y) ⊗ z) ≫
          (braiding F (G ⊛ H)).hom.app ((x ⊗ y) ⊗ z) ≫ (associator G H F).hom.app ((x ⊗ y) ⊗ z) =
    ((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) ≫
        (map (braiding F G).hom (𝟙 H)).app ((x ⊗ y) ⊗ z) ≫
          (associator G F H).hom.app ((x ⊗ y) ⊗ z) ≫ (map (𝟙 G) (braiding F H).hom).app ((x ⊗ y) ⊗ z)

Tactic:
simp only [whiskerLeft_id, Category.comp_id, associator_hom_unit_unit_assoc,
    externalProductBifunctor_obj_obj, tensor_obj, NatTrans.naturality_assoc,
    NatTrans.naturality, unit_app_braiding_hom_app_assoc,
    BraidedCategory.braiding_tensor_left_hom, Functor.map_comp, Category.assoc,
    Iso.map_hom_inv_id, BraidedCategory.braiding_naturality_right_assoc,
    BraidedCategory.braiding_tensor_right_hom, Iso.map_inv_hom_id_assoc,
    Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, unit_app_map_app_assoc,
    NatTrans.id_app, tensorHom_id]

Goal state after:
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
z x y : C
⊢ (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ (β_ (F.obj x) (H.obj z)).hom ≫
          G.obj y ◁ (unit H F).app (z, x) ≫
            (unit G (H ⊛ F)).app (y, z ⊗ x) ≫
              (G ⊛ H ⊛ F).map (y ◁ (β_ z x).hom) ≫ (G ⊛ H ⊛ F).map (α_ y x z).inv ≫ (G ⊛ H ⊛ F).map ((β_ y x).hom ▷ z) =
    (unit F G).app (x, y) ▷ H.obj z ≫
      (braiding F G).hom.app (x ⊗ y) ▷ H.obj z ≫
        (unit (G ⊛ F) H).app (x ⊗ y, z) ≫
          (associator G F H).hom.app ((x ⊗ y) ⊗ z) ≫ (map (𝟙 G) (braiding F H).hom).app ((x ⊗ y) ⊗ z)