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 ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ (𝟙 (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) ≫
        (associator F G H).inv.app (x ⊗ y ⊗ z) ≫
          (braiding (F ⊛ G) H).hom.app (x ⊗ y ⊗ z) ≫ (associator H F G).inv.app (x ⊗ y ⊗ z) =
    (𝟙 (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) ≫
        (map (𝟙 F) (braiding G H).hom).app (x ⊗ y ⊗ z) ≫
          (associator F H G).inv.app (x ⊗ y ⊗ z) ≫ (map (braiding F H).hom (𝟙 G)).app (x ⊗ y ⊗ z)

Tactic:
simp only [whiskerRight_tensor, id_whiskerRight, Category.id_comp,
    Iso.inv_hom_id, associator_inv_unit_unit_assoc,
    externalProductBifunctor_obj_obj, tensor_obj, NatTrans.naturality_assoc,
    NatTrans.naturality, unit_app_braiding_hom_app_assoc,
    BraidedCategory.braiding_tensor_right_hom, Functor.map_comp, Category.assoc,
    Iso.map_inv_hom_id, Category.comp_id,
    BraidedCategory.braiding_naturality_left_assoc,
    BraidedCategory.braiding_tensor_left_hom, Iso.map_hom_inv_id_assoc,
    Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc, unit_app_map_app_assoc,
    NatTrans.id_app, id_tensorHom]

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 ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ F.obj x ◁ (β_ (G.obj y) (H.obj z)).hom ≫
      (α_ (F.obj x) (H.obj z) (G.obj y)).inv ≫
        (β_ (F.obj x) (H.obj z)).hom ▷ G.obj y ≫
          (unit H F).app (z, x) ▷ G.obj y ≫
            (unit (H ⊛ F) G).app (z ⊗ x, y) ≫
              ((H ⊛ F) ⊛ G).map ((β_ z x).hom ▷ y) ≫
                ((H ⊛ F) ⊛ G).map (α_ x z y).hom ≫ ((H ⊛ F) ⊛ G).map (x ◁ (β_ z y).hom) =
    F.obj x ◁ (unit G H).app (y, z) ≫
      F.obj x ◁ (braiding G H).hom.app (y ⊗ z) ≫
        (unit F (H ⊛ G)).app (x, y ⊗ z) ≫
          (associator F H G).inv.app (x ⊗ y ⊗ z) ≫ (map (braiding F H).hom (𝟙 G)).app (x ⊗ y ⊗ z)